This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffin7-2

Description: Class form of isfin7-2 . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dffin7-2 FinVII = ( Fin ∪ ( V ∖ dom card ) )

Proof

Step Hyp Ref Expression
1 imor ⊢ ( ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
2 isfin7-2 ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ FinVII ↔ ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) ) )
3 2 elv ⊢ ( 𝑥 ∈ FinVII ↔ ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) )
4 elun ⊢ ( 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) ↔ ( 𝑥 ∈ Fin ∨ 𝑥 ∈ ( V ∖ dom card ) ) )
5 orcom ⊢ ( ( 𝑥 ∈ Fin ∨ 𝑥 ∈ ( V ∖ dom card ) ) ↔ ( 𝑥 ∈ ( V ∖ dom card ) ∨ 𝑥 ∈ Fin ) )
6 vex ⊢ 𝑥 ∈ V
7 eldif ⊢ ( 𝑥 ∈ ( V ∖ dom card ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom card ) )
8 6 7 mpbiran ⊢ ( 𝑥 ∈ ( V ∖ dom card ) ↔ ¬ 𝑥 ∈ dom card )
9 8 orbi1i ⊢ ( ( 𝑥 ∈ ( V ∖ dom card ) ∨ 𝑥 ∈ Fin ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
10 4 5 9 3bitri ⊢ ( 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
11 1 3 10 3bitr4i ⊢ ( 𝑥 ∈ FinVII ↔ 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) )
12 11 eqriv ⊢ FinVII = ( Fin ∪ ( V ∖ dom card ) )