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

Theorem r0weon 10007
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 6892 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (1st β€˜π‘₯) = (1st β€˜π‘§))
3 fveq2 6892 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘§))
42, 3uneq12d 4165 . . . . . . . . . . 11 (π‘₯ = 𝑧 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
5 eqid 2733 . . . . . . . . . . 11 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
6 fvex 6905 . . . . . . . . . . . 12 (1st β€˜π‘§) ∈ V
7 fvex 6905 . . . . . . . . . . . 12 (2nd β€˜π‘§) ∈ V
86, 7unex 7733 . . . . . . . . . . 11 ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ V
94, 5, 8fvmpt 6999 . . . . . . . . . 10 (𝑧 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
10 fveq2 6892 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (1st β€˜π‘₯) = (1st β€˜π‘€))
11 fveq2 6892 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘€))
1210, 11uneq12d 4165 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
13 fvex 6905 . . . . . . . . . . . 12 (1st β€˜π‘€) ∈ V
14 fvex 6905 . . . . . . . . . . . 12 (2nd β€˜π‘€) ∈ V
1513, 14unex 7733 . . . . . . . . . . 11 ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ V
1612, 5, 15fvmpt 6999 . . . . . . . . . 10 (𝑀 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
179, 16breqan12d 5165 . . . . . . . . 9 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) E ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
1815epeli 5583 . . . . . . . . 9 (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) E ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
1917, 18bitrdi 287 . . . . . . . 8 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
209, 16eqeqan12d 2747 . . . . . . . . 9 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
2120anbi1d 631 . . . . . . . 8 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ ((((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀) ↔ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))
2219, 21orbi12d 918 . . . . . . 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 576 . . . . . 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 5216 . . . . 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 2764 . . . 4 𝑅 = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∨ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ∧ 𝑧𝐿𝑀)))}
26 xp1st 8007 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (1st β€˜π‘₯) ∈ On)
27 xp2nd 8008 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (2nd β€˜π‘₯) ∈ On)
28 fvex 6905 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
2928elon 6374 . . . . . . . . 9 ((1st β€˜π‘₯) ∈ On ↔ Ord (1st β€˜π‘₯))
30 fvex 6905 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
3130elon 6374 . . . . . . . . 9 ((2nd β€˜π‘₯) ∈ On ↔ Ord (2nd β€˜π‘₯))
32 ordun 6469 . . . . . . . . 9 ((Ord (1st β€˜π‘₯) ∧ Ord (2nd β€˜π‘₯)) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3329, 31, 32syl2anb 599 . . . . . . . 8 (((1st β€˜π‘₯) ∈ On ∧ (2nd β€˜π‘₯) ∈ On) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3426, 27, 33syl2anc 585 . . . . . . 7 (π‘₯ ∈ (On Γ— On) β†’ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3528, 30unex 7733 . . . . . . . 8 ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ V
3635elon 6374 . . . . . . 7 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On ↔ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3734, 36sylibr 233 . . . . . 6 (π‘₯ ∈ (On Γ— On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On)
385, 37fmpti 7112 . . . . 5 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On
3938a1i 11 . . . 4 (⊀ β†’ (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On)
40 epweon 7762 . . . . 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 10006 . . . . 5 𝐿 We (On Γ— On)
4443a1i 11 . . . 4 (⊀ β†’ 𝐿 We (On Γ— On))
45 vex 3479 . . . . . . . 8 𝑒 ∈ V
4645dmex 7902 . . . . . . 7 dom 𝑒 ∈ V
4745rnex 7903 . . . . . . 7 ran 𝑒 ∈ V
4846, 47unex 7733 . . . . . 6 (dom 𝑒 βˆͺ ran 𝑒) ∈ V
49 imadmres 6234 . . . . . . 7 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒)
50 inss2 4230 . . . . . . . . . 10 (𝑒 ∩ (On Γ— On)) βŠ† (On Γ— On)
51 ssun1 4173 . . . . . . . . . . . . . 14 dom 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
52 elinel2 4197 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ (On Γ— On))
53 1st2nd2 8014 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (On Γ— On) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
5452, 53syl 17 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
55 elinel1 4196 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ 𝑒)
5654, 55eqeltrrd 2835 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒)
5728, 30opeldm 5908 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5856, 57syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5951, 58sselid 3981 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
60 ssun2 4174 . . . . . . . . . . . . . 14 ran 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
6128, 30opelrn 5943 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6256, 61syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6360, 62sselid 3981 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
6459, 63prssd 4826 . . . . . . . . . . . 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 7814 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) ∈ On ∧ (2nd β€˜π‘₯) ∈ On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6865, 66, 67syl2anc 585 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6964, 68sseldd 3984 . . . . . . . . . . 11 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒))
7069rgen 3064 . . . . . . . . . 10 βˆ€π‘₯ ∈ (𝑒 ∩ (On Γ— On))((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)
71 ssrab 4071 . . . . . . . . . 10 ((𝑒 ∩ (On Γ— On)) βŠ† {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)} ↔ ((𝑒 ∩ (On Γ— On)) βŠ† (On Γ— On) ∧ βˆ€π‘₯ ∈ (𝑒 ∩ (On Γ— On))((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)))
7250, 70, 71mpbir2an 710 . . . . . . . . 9 (𝑒 ∩ (On Γ— On)) βŠ† {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)}
73 dmres 6004 . . . . . . . . . 10 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))))
7438fdmi 6730 . . . . . . . . . . 11 dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (On Γ— On)
7574ineq2i 4210 . . . . . . . . . 10 (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))) = (𝑒 ∩ (On Γ— On))
7673, 75eqtri 2761 . . . . . . . . 9 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ (On Γ— On))
775mptpreima 6238 . . . . . . . . 9 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒)) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)}
7872, 76, 773sstr4i 4026 . . . . . . . 8 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒))
79 funmpt 6587 . . . . . . . . 9 Fun (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
80 resss 6007 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
81 dmss 5903 . . . . . . . . . 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 7056 . . . . . . . . 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 691 . . . . . . . 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 4018 . . . . . 6 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (dom 𝑒 βˆͺ ran 𝑒)
8748, 86ssexi 5323 . . . . 5 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
8887a1i 11 . . . 4 (⊀ β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
8925, 39, 41, 44, 88fnwe 8118 . . 3 (⊀ β†’ 𝑅 We (On Γ— On))
90 epse 5660 . . . . 5 E Se On
9190a1i 11 . . . 4 (⊀ β†’ E Se On)
92 vuniex 7729 . . . . . . . 8 βˆͺ 𝑒 ∈ V
9392pwex 5379 . . . . . . 7 𝒫 βˆͺ 𝑒 ∈ V
9493, 93xpex 7740 . . . . . 6 (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ∈ V
955mptpreima 6238 . . . . . . . 8 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒}
96 df-rab 3434 . . . . . . . 8 {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒} = {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)}
9795, 96eqtri 2761 . . . . . . 7 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) = {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)}
9853adantr 482 . . . . . . . . 9 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
99 elssuni 4942 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
10099adantl 483 . . . . . . . . . . . 12 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
101100unssad 4188 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
10228elpw 4607 . . . . . . . . . . 11 ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
103101, 102sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
104100unssbd 4189 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
10530elpw 4607 . . . . . . . . . . 11 ((2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
106104, 105sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
107103, 106jca 513 . . . . . . . . 9 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒))
108 elxp6 8009 . . . . . . . . 9 (π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ↔ (π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∧ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)))
10998, 107, 108sylanbrc 584 . . . . . . . 8 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒))
110109abssi 4068 . . . . . . 7 {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)} βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11197, 110eqsstri 4017 . . . . . 6 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11294, 111ssexi 5323 . . . . 5 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
113112a1i 11 . . . 4 (⊀ β†’ (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
11425, 39, 91, 113fnse 8119 . . 3 (⊀ β†’ 𝑅 Se (On Γ— On))
11589, 114jca 513 . 2 (⊀ β†’ (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On)))
116115mptru 1549 1 (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  {crab 3433  Vcvv 3475   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  {cpr 4631  βŸ¨cop 4635  βˆͺ cuni 4909   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   E cep 5580   Se wse 5630   We wwe 5631   Γ— cxp 5675  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680  Ord word 6364  Oncon0 6365  Fun wfun 6538  βŸΆwf 6540  β€˜cfv 6544  1st c1st 7973  2nd c2nd 7974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-1st 7975  df-2nd 7976
This theorem is referenced by:  infxpenlem  10008
  Copyright terms: Public domain W3C validator