Metamath Proof Explorer

Theorem dffin7-2

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

Ref Expression
Assertion dffin7-2 
|- Fin7 = ( Fin u. ( _V \ dom card ) )

Proof

Step Hyp Ref Expression
1 imor 
 |-  ( ( x e. dom card -> x e. Fin ) <-> ( -. x e. dom card \/ x e. Fin ) )
2 isfin7-2 
 |-  ( x e. _V -> ( x e. Fin7 <-> ( x e. dom card -> x e. Fin ) ) )
3 2 elv 
 |-  ( x e. Fin7 <-> ( x e. dom card -> x e. Fin ) )
4 elun 
 |-  ( x e. ( Fin u. ( _V \ dom card ) ) <-> ( x e. Fin \/ x e. ( _V \ dom card ) ) )
5 orcom 
 |-  ( ( x e. Fin \/ x e. ( _V \ dom card ) ) <-> ( x e. ( _V \ dom card ) \/ x e. Fin ) )
6 vex 
 |-  x e. _V
7 eldif 
 |-  ( x e. ( _V \ dom card ) <-> ( x e. _V /\ -. x e. dom card ) )
8 6 7 mpbiran 
 |-  ( x e. ( _V \ dom card ) <-> -. x e. dom card )
9 8 orbi1i 
 |-  ( ( x e. ( _V \ dom card ) \/ x e. Fin ) <-> ( -. x e. dom card \/ x e. Fin ) )
10 4 5 9 3bitri 
 |-  ( x e. ( Fin u. ( _V \ dom card ) ) <-> ( -. x e. dom card \/ x e. Fin ) )
11 1 3 10 3bitr4i 
 |-  ( x e. Fin7 <-> x e. ( Fin u. ( _V \ dom card ) ) )
12 11 eqriv 
 |-  Fin7 = ( Fin u. ( _V \ dom card ) )