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