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β‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE

Proof

Step Hyp Ref Expression
1 dfon2 ⊒On=x|βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x
2 eqabcb ⊒x|βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x=Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEβ†”βˆ€xβˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x↔x∈Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
3 vex ⊒x∈V
4 3 elrn ⊒x∈ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEβ†”βˆƒyyπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEx
5 brin ⊒yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔y𝖲𝖲𝖾𝗍x∧yπ–³π—‹π–Ίπ—‡π—ŒΓ—Vx
6 3 brsset ⊒y𝖲𝖲𝖾𝗍x↔yβŠ†x
7 brxp ⊒yπ–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔yβˆˆπ–³π—‹π–Ίπ—‡π—Œβˆ§x∈V
8 3 7 mpbiran2 ⊒yπ–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔yβˆˆπ–³π—‹π–Ίπ—‡π—Œ
9 vex ⊒y∈V
10 9 eltrans ⊒yβˆˆπ–³π—‹π–Ίπ—‡π—Œβ†”Tr⁑y
11 8 10 bitri ⊒yπ–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔Tr⁑y
12 6 11 anbi12i ⊒y𝖲𝖲𝖾𝗍x∧yπ–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔yβŠ†x∧Tr⁑y
13 5 12 bitri ⊒yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vx↔yβŠ†x∧Tr⁑y
14 ioran ⊒¬y=x∨y∈x↔¬y=x∧¬y∈x
15 brun ⊒yIβˆͺEx↔yIx∨yEx
16 3 ideq ⊒yIx↔y=x
17 epel ⊒yEx↔y∈x
18 16 17 orbi12i ⊒yIx∨yEx↔y=x∨y∈x
19 15 18 bitri ⊒yIβˆͺEx↔y=x∨y∈x
20 14 19 xchnxbir ⊒¬yIβˆͺEx↔¬y=x∧¬y∈x
21 13 20 anbi12i ⊒yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vx∧¬yIβˆͺEx↔yβŠ†x∧Tr⁑y∧¬y=x∧¬y∈x
22 brdif ⊒yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEx↔yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vx∧¬yIβˆͺEx
23 dfpss2 ⊒yβŠ‚x↔yβŠ†x∧¬y=x
24 23 anbi1i ⊒yβŠ‚x∧Tr⁑y↔yβŠ†x∧¬y=x∧Tr⁑y
25 an32 ⊒yβŠ†x∧¬y=x∧Tr⁑y↔yβŠ†x∧Tr⁑y∧¬y=x
26 24 25 bitri ⊒yβŠ‚x∧Tr⁑y↔yβŠ†x∧Tr⁑y∧¬y=x
27 26 anbi1i ⊒yβŠ‚x∧Tr⁑y∧¬y∈x↔yβŠ†x∧Tr⁑y∧¬y=x∧¬y∈x
28 anass ⊒yβŠ†x∧Tr⁑y∧¬y=x∧¬y∈x↔yβŠ†x∧Tr⁑y∧¬y=x∧¬y∈x
29 27 28 bitri ⊒yβŠ‚x∧Tr⁑y∧¬y∈x↔yβŠ†x∧Tr⁑y∧¬y=x∧¬y∈x
30 21 22 29 3bitr4i ⊒yπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEx↔yβŠ‚x∧Tr⁑y∧¬y∈x
31 30 exbii βŠ’βˆƒyyπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺExβ†”βˆƒyyβŠ‚x∧Tr⁑y∧¬y∈x
32 exanali βŠ’βˆƒyyβŠ‚x∧Tr⁑y∧¬y∈xβ†”Β¬βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x
33 31 32 bitri βŠ’βˆƒyyπ–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺExβ†”Β¬βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x
34 4 33 bitri ⊒x∈ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺEβ†”Β¬βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x
35 34 con2bii βŠ’βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x↔¬x∈ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
36 eldif ⊒x∈Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE↔x∈V∧¬x∈ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
37 3 36 mpbiran ⊒x∈Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE↔¬x∈ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
38 35 37 bitr4i βŠ’βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x↔x∈Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
39 2 38 mpgbir ⊒x|βˆ€yyβŠ‚x∧Tr⁑yβ†’y∈x=Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
40 1 39 eqtri ⊒On=Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE