Metamath Proof Explorer

Theorem dfon3

Description: A quantifier-free definition of On . (Contributed by Scott Fenton, 5-Apr-2012)

Ref Expression
Assertion dfon3 
|- On = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )

Proof

Step Hyp Ref Expression
1 dfon2 
 |-  On = { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) }
2 abeq1 
 |-  ( { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) } = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) <-> A. x ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) <-> x e. ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) ) )
3 vex 
 |-  x e. _V
4 3 elrn 
 |-  ( x e. ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) <-> E. y y ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) x )
5 brin 
 |-  ( y ( SSet i^i ( Trans X. _V ) ) x <-> ( y SSet x /\ y ( Trans X. _V ) x ) )
6 3 brsset 
 |-  ( y SSet x <-> y C_ x )
7 brxp 
 |-  ( y ( Trans X. _V ) x <-> ( y e. Trans /\ x e. _V ) )
8 3 7 mpbiran2 
 |-  ( y ( Trans X. _V ) x <-> y e. Trans )
9 vex 
 |-  y e. _V
10 9 eltrans 
 |-  ( y e. Trans <-> Tr y )
11 8 10 bitri 
 |-  ( y ( Trans X. _V ) x <-> Tr y )
12 6 11 anbi12i 
 |-  ( ( y SSet x /\ y ( Trans X. _V ) x ) <-> ( y C_ x /\ Tr y ) )
13 5 12 bitri 
 |-  ( y ( SSet i^i ( Trans X. _V ) ) x <-> ( y C_ x /\ Tr y ) )
14 ioran 
 |-  ( -. ( y = x \/ y e. x ) <-> ( -. y = x /\ -. y e. x ) )
15 brun 
 |-  ( y ( _I u. _E ) x <-> ( y _I x \/ y _E x ) )
16 3 ideq 
 |-  ( y _I x <-> y = x )
17 epel 
 |-  ( y _E x <-> y e. x )
18 16 17 orbi12i 
 |-  ( ( y _I x \/ y _E x ) <-> ( y = x \/ y e. x ) )
19 15 18 bitri 
 |-  ( y ( _I u. _E ) x <-> ( y = x \/ y e. x ) )
20 14 19 xchnxbir 
 |-  ( -. y ( _I u. _E ) x <-> ( -. y = x /\ -. y e. x ) )
21 13 20 anbi12i 
 |-  ( ( y ( SSet i^i ( Trans X. _V ) ) x /\ -. y ( _I u. _E ) x ) <-> ( ( y C_ x /\ Tr y ) /\ ( -. y = x /\ -. y e. x ) ) )
22 brdif 
 |-  ( y ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) x <-> ( y ( SSet i^i ( Trans X. _V ) ) x /\ -. y ( _I u. _E ) x ) )
23 dfpss2 
 |-  ( y C. x <-> ( y C_ x /\ -. y = x ) )
24 23 anbi1i 
 |-  ( ( y C. x /\ Tr y ) <-> ( ( y C_ x /\ -. y = x ) /\ Tr y ) )
25 an32 
 |-  ( ( ( y C_ x /\ -. y = x ) /\ Tr y ) <-> ( ( y C_ x /\ Tr y ) /\ -. y = x ) )
26 24 25 bitri 
 |-  ( ( y C. x /\ Tr y ) <-> ( ( y C_ x /\ Tr y ) /\ -. y = x ) )
27 26 anbi1i 
 |-  ( ( ( y C. x /\ Tr y ) /\ -. y e. x ) <-> ( ( ( y C_ x /\ Tr y ) /\ -. y = x ) /\ -. y e. x ) )
28 anass 
 |-  ( ( ( ( y C_ x /\ Tr y ) /\ -. y = x ) /\ -. y e. x ) <-> ( ( y C_ x /\ Tr y ) /\ ( -. y = x /\ -. y e. x ) ) )
29 27 28 bitri 
 |-  ( ( ( y C. x /\ Tr y ) /\ -. y e. x ) <-> ( ( y C_ x /\ Tr y ) /\ ( -. y = x /\ -. y e. x ) ) )
30 21 22 29 3bitr4i 
 |-  ( y ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) x <-> ( ( y C. x /\ Tr y ) /\ -. y e. x ) )
31 30 exbii 
 |-  ( E. y y ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) x <-> E. y ( ( y C. x /\ Tr y ) /\ -. y e. x ) )
32 exanali 
 |-  ( E. y ( ( y C. x /\ Tr y ) /\ -. y e. x ) <-> -. A. y ( ( y C. x /\ Tr y ) -> y e. x ) )
33 31 32 bitri 
 |-  ( E. y y ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) x <-> -. A. y ( ( y C. x /\ Tr y ) -> y e. x ) )
34 4 33 bitri 
 |-  ( x e. ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) <-> -. A. y ( ( y C. x /\ Tr y ) -> y e. x ) )
35 34 con2bii 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) <-> -. x e. ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
36 eldif 
 |-  ( x e. ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) <-> ( x e. _V /\ -. x e. ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) )
37 3 36 mpbiran 
 |-  ( x e. ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) <-> -. x e. ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
38 35 37 bitr4i 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) <-> x e. ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) ) )
39 2 38 mpgbir 
 |-  { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) } = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
40 1 39 eqtri 
 |-  On = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )