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 ⊢ x ∈ dom ⁡ card → x ∈ Fin ↔ ¬ x ∈ dom ⁡ card ∨ x ∈ Fin
2 isfin7-2 ⊢ x ∈ V → x ∈ FinVII ↔ x ∈ dom ⁡ card → x ∈ Fin
3 2 elv ⊢ x ∈ FinVII ↔ x ∈ dom ⁡ card → x ∈ Fin
4 elun ⊢ x ∈ Fin ∪ V ∖ dom ⁡ card ↔ x ∈ Fin ∨ x ∈ V ∖ dom ⁡ card
5 orcom ⊢ x ∈ Fin ∨ x ∈ V ∖ dom ⁡ card ↔ x ∈ V ∖ dom ⁡ card ∨ x ∈ Fin
6 vex ⊢ x ∈ V
7 eldif ⊢ x ∈ V ∖ dom ⁡ card ↔ x ∈ V ∧ ¬ x ∈ dom ⁡ card
8 6 7 mpbiran ⊢ x ∈ V ∖ dom ⁡ card ↔ ¬ x ∈ dom ⁡ card
9 8 orbi1i ⊢ x ∈ V ∖ dom ⁡ card ∨ x ∈ Fin ↔ ¬ x ∈ dom ⁡ card ∨ x ∈ Fin
10 4 5 9 3bitri ⊢ x ∈ Fin ∪ V ∖ dom ⁡ card ↔ ¬ x ∈ dom ⁡ card ∨ x ∈ Fin
11 1 3 10 3bitr4i ⊢ x ∈ FinVII ↔ x ∈ Fin ∪ V ∖ dom ⁡ card
12 11 eqriv ⊢ FinVII = Fin ∪ V ∖ dom ⁡ card