MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r0weon Structured version   Visualization version   GIF version

Theorem r0weon 10009
Description: A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of [TakeutiZaring] p. 54. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
leweon.1 𝐿 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (On Γ— On) ∧ 𝑦 ∈ (On Γ— On)) ∧ ((1st β€˜π‘₯) ∈ (1st β€˜π‘¦) ∨ ((1st β€˜π‘₯) = (1st β€˜π‘¦) ∧ (2nd β€˜π‘₯) ∈ (2nd β€˜π‘¦))))}
r0weon.1 𝑅 = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))}
Assertion
Ref Expression
r0weon (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On))
Distinct variable groups:   𝑧,𝑀,𝐿   π‘₯,𝑀,𝑦,𝑧
Allowed substitution hints:   𝑅(π‘₯,𝑦,𝑧,𝑀)   𝐿(π‘₯,𝑦)

Proof of Theorem r0weon
Dummy variable 𝑒 is distinct from all other variables.
StepHypRef Expression
1 r0weon.1 . . . . 5 𝑅 = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))}
2 fveq2 6891 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (1st β€˜π‘₯) = (1st β€˜π‘§))
3 fveq2 6891 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘§))
42, 3uneq12d 4164 . . . . . . . . . . 11 (π‘₯ = 𝑧 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
5 eqid 2732 . . . . . . . . . . 11 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
6 fvex 6904 . . . . . . . . . . . 12 (1st β€˜π‘§) ∈ V
7 fvex 6904 . . . . . . . . . . . 12 (2nd β€˜π‘§) ∈ V
86, 7unex 7735 . . . . . . . . . . 11 ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ V
94, 5, 8fvmpt 6998 . . . . . . . . . 10 (𝑧 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
10 fveq2 6891 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (1st β€˜π‘₯) = (1st β€˜π‘€))
11 fveq2 6891 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘€))
1210, 11uneq12d 4164 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
13 fvex 6904 . . . . . . . . . . . 12 (1st β€˜π‘€) ∈ V
14 fvex 6904 . . . . . . . . . . . 12 (2nd β€˜π‘€) ∈ V
1513, 14unex 7735 . . . . . . . . . . 11 ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ V
1612, 5, 15fvmpt 6998 . . . . . . . . . 10 (𝑀 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
179, 16breqan12d 5164 . . . . . . . . 9 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) E ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
1815epeli 5582 . . . . . . . . 9 (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) E ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
1917, 18bitrdi 286 . . . . . . . 8 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
209, 16eqeqan12d 2746 . . . . . . . . 9 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
2120anbi1d 630 . . . . . . . 8 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ ((((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀) ↔ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))
2219, 21orbi12d 917 . . . . . . 7 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ ((((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∨ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀)) ↔ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀))))
2322pm5.32i 575 . . . . . 6 (((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∨ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀))) ↔ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀))))
2423opabbii 5215 . . . . 5 {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∨ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀)))} = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))}
251, 24eqtr4i 2763 . . . 4 𝑅 = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∨ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀)))}
26 xp1st 8009 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (1st β€˜π‘₯) ∈ On)
27 xp2nd 8010 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (2nd β€˜π‘₯) ∈ On)
28 fvex 6904 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
2928elon 6373 . . . . . . . . 9 ((1st β€˜π‘₯) ∈ On ↔ Ord (1st β€˜π‘₯))
30 fvex 6904 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
3130elon 6373 . . . . . . . . 9 ((2nd β€˜π‘₯) ∈ On ↔ Ord (2nd β€˜π‘₯))
32 ordun 6468 . . . . . . . . 9 ((Ord (1st β€˜π‘₯) ∧ Ord (2nd β€˜π‘₯)) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3329, 31, 32syl2anb 598 . . . . . . . 8 (((1st β€˜π‘₯) ∈ On ∧ (2nd β€˜π‘₯) ∈ On) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3426, 27, 33syl2anc 584 . . . . . . 7 (π‘₯ ∈ (On Γ— On) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3528, 30unex 7735 . . . . . . . 8 ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ V
3635elon 6373 . . . . . . 7 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On ↔ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3734, 36sylibr 233 . . . . . 6 (π‘₯ ∈ (On Γ— On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On)
385, 37fmpti 7113 . . . . 5 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On
3938a1i 11 . . . 4 (⊀ β†’ (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On)
40 epweon 7764 . . . . 5 E We On
4140a1i 11 . . . 4 (⊀ β†’ E We On)
42 leweon.1 . . . . . 6 𝐿 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (On Γ— On) ∧ 𝑦 ∈ (On Γ— On)) ∧ ((1st β€˜π‘₯) ∈ (1st β€˜π‘¦) ∨ ((1st β€˜π‘₯) = (1st β€˜π‘¦) ∧ (2nd β€˜π‘₯) ∈ (2nd β€˜π‘¦))))}
4342leweon 10008 . . . . 5 𝐿 We (On Γ— On)
4443a1i 11 . . . 4 (⊀ β†’ 𝐿 We (On Γ— On))
45 vex 3478 . . . . . . . 8 𝑒 ∈ V
4645dmex 7904 . . . . . . 7 dom 𝑒 ∈ V
4745rnex 7905 . . . . . . 7 ran 𝑒 ∈ V
4846, 47unex 7735 . . . . . 6 (dom 𝑒 βˆͺ ran 𝑒) ∈ V
49 imadmres 6233 . . . . . . 7 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒)
50 inss2 4229 . . . . . . . . . 10 (𝑒 ∩ (On Γ— On)) βŠ† (On Γ— On)
51 ssun1 4172 . . . . . . . . . . . . . 14 dom 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
52 elinel2 4196 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ (On Γ— On))
53 1st2nd2 8016 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (On Γ— On) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
5452, 53syl 17 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
55 elinel1 4195 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ 𝑒)
5654, 55eqeltrrd 2834 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒)
5728, 30opeldm 5907 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5856, 57syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5951, 58sselid 3980 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
60 ssun2 4173 . . . . . . . . . . . . . 14 ran 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
6128, 30opelrn 5942 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6256, 61syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6360, 62sselid 3980 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
6459, 63prssd 4825 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ {(1st β€˜π‘₯), (2nd β€˜π‘₯)} βŠ† (dom 𝑒 βˆͺ ran 𝑒))
6552, 26syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ On)
6652, 27syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ On)
67 ordunpr 7816 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) ∈ On ∧ (2nd β€˜π‘₯) ∈ On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6865, 66, 67syl2anc 584 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6964, 68sseldd 3983 . . . . . . . . . . 11 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒))
7069rgen 3063 . . . . . . . . . 10 βˆ€π‘₯ ∈ (𝑒 ∩ (On Γ— On))((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)
71 ssrab 4070 . . . . . . . . . 10 ((𝑒 ∩ (On Γ— On)) βŠ† {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)} ↔ ((𝑒 ∩ (On Γ— On)) βŠ† (On Γ— On) ∧ βˆ€π‘₯ ∈ (𝑒 ∩ (On Γ— On))((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)))
7250, 70, 71mpbir2an 709 . . . . . . . . 9 (𝑒 ∩ (On Γ— On)) βŠ† {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)}
73 dmres 6003 . . . . . . . . . 10 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))))
7438fdmi 6729 . . . . . . . . . . 11 dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (On Γ— On)
7574ineq2i 4209 . . . . . . . . . 10 (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))) = (𝑒 ∩ (On Γ— On))
7673, 75eqtri 2760 . . . . . . . . 9 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ (On Γ— On))
775mptpreima 6237 . . . . . . . . 9 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒)) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)}
7872, 76, 773sstr4i 4025 . . . . . . . 8 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒))
79 funmpt 6586 . . . . . . . . 9 Fun (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
80 resss 6006 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
81 dmss 5902 . . . . . . . . . 10 (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†’ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))))
8280, 81ax-mp 5 . . . . . . . . 9 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
83 funimass3 7055 . . . . . . . . 9 ((Fun (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) ∧ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) βŠ† (dom 𝑒 βˆͺ ran 𝑒) ↔ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒))))
8479, 82, 83mp2an 690 . . . . . . . 8 (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) βŠ† (dom 𝑒 βˆͺ ran 𝑒) ↔ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒)))
8578, 84mpbir 230 . . . . . . 7 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) βŠ† (dom 𝑒 βˆͺ ran 𝑒)
8649, 85eqsstrri 4017 . . . . . 6 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (dom 𝑒 βˆͺ ran 𝑒)
8748, 86ssexi 5322 . . . . 5 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
8887a1i 11 . . . 4 (⊀ β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
8925, 39, 41, 44, 88fnwe 8120 . . 3 (⊀ β†’ 𝑅 We (On Γ— On))
90 epse 5659 . . . . 5 E Se On
9190a1i 11 . . . 4 (⊀ β†’ E Se On)
92 vuniex 7731 . . . . . . . 8 βˆͺ 𝑒 ∈ V
9392pwex 5378 . . . . . . 7 𝒫 βˆͺ 𝑒 ∈ V
9493, 93xpex 7742 . . . . . 6 (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ∈ V
955mptpreima 6237 . . . . . . . 8 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒}
96 df-rab 3433 . . . . . . . 8 {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒} = {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)}
9795, 96eqtri 2760 . . . . . . 7 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) = {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)}
9853adantr 481 . . . . . . . . 9 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
99 elssuni 4941 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
10099adantl 482 . . . . . . . . . . . 12 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
101100unssad 4187 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
10228elpw 4606 . . . . . . . . . . 11 ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
103101, 102sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
104100unssbd 4188 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
10530elpw 4606 . . . . . . . . . . 11 ((2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
106104, 105sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
107103, 106jca 512 . . . . . . . . 9 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒))
108 elxp6 8011 . . . . . . . . 9 (π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ↔ (π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∧ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)))
10998, 107, 108sylanbrc 583 . . . . . . . 8 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒))
110109abssi 4067 . . . . . . 7 {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)} βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11197, 110eqsstri 4016 . . . . . 6 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11294, 111ssexi 5322 . . . . 5 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
113112a1i 11 . . . 4 (⊀ β†’ (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
11425, 39, 91, 113fnse 8121 . . 3 (⊀ β†’ 𝑅 Se (On Γ— On))
11589, 114jca 512 . 2 (⊀ β†’ (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On)))
116115mptru 1548 1 (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602  {cpr 4630  βŸ¨cop 4634  βˆͺ cuni 4908   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   E cep 5579   Se wse 5629   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Ord word 6363  Oncon0 6364  Fun wfun 6537  βŸΆwf 6539  β€˜cfv 6543  1st c1st 7975  2nd c2nd 7976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-1st 7977  df-2nd 7978
This theorem is referenced by:  infxpenlem  10010
  Copyright terms: Public domain W3C validator