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 ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )

Proof

Step Hyp Ref Expression
1 dfon2 ⊢ On = { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) }
2 abeq1 ⊢ ( { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) } = ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) ↔ ∀ 𝑥 ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ↔ 𝑥 ∈ ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) ) )
3 vex ⊢ 𝑥 ∈ V
4 3 elrn ⊢ ( 𝑥 ∈ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ↔ ∃ 𝑦 𝑦 ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) 𝑥 )
5 brin ⊢ ( 𝑦 ( SSet ∩ ( Trans × V ) ) 𝑥 ↔ ( 𝑦 SSet 𝑥 ∧ 𝑦 ( Trans × V ) 𝑥 ) )
6 3 brsset ⊢ ( 𝑦 SSet 𝑥 ↔ 𝑦 ⊆ 𝑥 )
7 brxp ⊢ ( 𝑦 ( Trans × V ) 𝑥 ↔ ( 𝑦 ∈ Trans ∧ 𝑥 ∈ V ) )
8 3 7 mpbiran2 ⊢ ( 𝑦 ( Trans × V ) 𝑥 ↔ 𝑦 ∈ Trans )
9 vex ⊢ 𝑦 ∈ V
10 9 eltrans ⊢ ( 𝑦 ∈ Trans ↔ Tr 𝑦 )
11 8 10 bitri ⊢ ( 𝑦 ( Trans × V ) 𝑥 ↔ Tr 𝑦 )
12 6 11 anbi12i ⊢ ( ( 𝑦 SSet 𝑥 ∧ 𝑦 ( Trans × V ) 𝑥 ) ↔ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) )
13 5 12 bitri ⊢ ( 𝑦 ( SSet ∩ ( Trans × V ) ) 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) )
14 ioran ⊢ ( ¬ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) ↔ ( ¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) )
15 brun ⊢ ( 𝑦 ( I ∪ E ) 𝑥 ↔ ( 𝑦 I 𝑥 ∨ 𝑦 E 𝑥 ) )
16 3 ideq ⊢ ( 𝑦 I 𝑥 ↔ 𝑦 = 𝑥 )
17 epel ⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
18 16 17 orbi12i ⊢ ( ( 𝑦 I 𝑥 ∨ 𝑦 E 𝑥 ) ↔ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) )
19 15 18 bitri ⊢ ( 𝑦 ( I ∪ E ) 𝑥 ↔ ( 𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥 ) )
20 14 19 xchnxbir ⊢ ( ¬ 𝑦 ( I ∪ E ) 𝑥 ↔ ( ¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) )
21 13 20 anbi12i ⊢ ( ( 𝑦 ( SSet ∩ ( Trans × V ) ) 𝑥 ∧ ¬ 𝑦 ( I ∪ E ) 𝑥 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ( ¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) ) )
22 brdif ⊢ ( 𝑦 ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) 𝑥 ↔ ( 𝑦 ( SSet ∩ ( Trans × V ) ) 𝑥 ∧ ¬ 𝑦 ( I ∪ E ) 𝑥 ) )
23 dfpss2 ⊢ ( 𝑦 ⊊ 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥 ) )
24 23 anbi1i ⊢ ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥 ) ∧ Tr 𝑦 ) )
25 an32 ⊢ ( ( ( 𝑦 ⊆ 𝑥 ∧ ¬ 𝑦 = 𝑥 ) ∧ Tr 𝑦 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 = 𝑥 ) )
26 24 25 bitri ⊢ ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 = 𝑥 ) )
27 26 anbi1i ⊢ ( ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 ∈ 𝑥 ) ↔ ( ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 = 𝑥 ) ∧ ¬ 𝑦 ∈ 𝑥 ) )
28 anass ⊢ ( ( ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 = 𝑥 ) ∧ ¬ 𝑦 ∈ 𝑥 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ( ¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) ) )
29 27 28 bitri ⊢ ( ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 ∈ 𝑥 ) ↔ ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑦 ) ∧ ( ¬ 𝑦 = 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) ) )
30 21 22 29 3bitr4i ⊢ ( 𝑦 ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) 𝑥 ↔ ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 ∈ 𝑥 ) )
31 30 exbii ⊢ ( ∃ 𝑦 𝑦 ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) 𝑥 ↔ ∃ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 ∈ 𝑥 ) )
32 exanali ⊢ ( ∃ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) ∧ ¬ 𝑦 ∈ 𝑥 ) ↔ ¬ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
33 31 32 bitri ⊢ ( ∃ 𝑦 𝑦 ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) 𝑥 ↔ ¬ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
34 4 33 bitri ⊢ ( 𝑥 ∈ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ↔ ¬ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) )
35 34 con2bii ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ↔ ¬ 𝑥 ∈ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )
36 eldif ⊢ ( 𝑥 ∈ ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) )
37 3 36 mpbiran ⊢ ( 𝑥 ∈ ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) ↔ ¬ 𝑥 ∈ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )
38 35 37 bitr4i ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ↔ 𝑥 ∈ ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) ) )
39 2 38 mpgbir ⊢ { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) } = ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )
40 1 39 eqtri ⊢ On = ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )