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

Theorem r0weon 9953
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 6843 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (1st β€˜π‘₯) = (1st β€˜π‘§))
3 fveq2 6843 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘§))
42, 3uneq12d 4125 . . . . . . . . . . 11 (π‘₯ = 𝑧 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
5 eqid 2733 . . . . . . . . . . 11 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
6 fvex 6856 . . . . . . . . . . . 12 (1st β€˜π‘§) ∈ V
7 fvex 6856 . . . . . . . . . . . 12 (2nd β€˜π‘§) ∈ V
86, 7unex 7681 . . . . . . . . . . 11 ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ V
94, 5, 8fvmpt 6949 . . . . . . . . . 10 (𝑧 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) = ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
10 fveq2 6843 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (1st β€˜π‘₯) = (1st β€˜π‘€))
11 fveq2 6843 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (2nd β€˜π‘₯) = (2nd β€˜π‘€))
1210, 11uneq12d 4125 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
13 fvex 6856 . . . . . . . . . . . 12 (1st β€˜π‘€) ∈ V
14 fvex 6856 . . . . . . . . . . . 12 (2nd β€˜π‘€) ∈ V
1513, 14unex 7681 . . . . . . . . . . 11 ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ V
1612, 5, 15fvmpt 6949 . . . . . . . . . 10 (𝑀 ∈ (On Γ— On) β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
179, 16breqan12d 5122 . . . . . . . . 9 ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) β†’ (((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘§) E ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))β€˜π‘€) ↔ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) E ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
1815epeli 5540 . . . . . . . . 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 5173 . . . . 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 7954 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (1st β€˜π‘₯) ∈ On)
27 xp2nd 7955 . . . . . . . 8 (π‘₯ ∈ (On Γ— On) β†’ (2nd β€˜π‘₯) ∈ On)
28 fvex 6856 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
2928elon 6327 . . . . . . . . 9 ((1st β€˜π‘₯) ∈ On ↔ Ord (1st β€˜π‘₯))
30 fvex 6856 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
3130elon 6327 . . . . . . . . 9 ((2nd β€˜π‘₯) ∈ On ↔ Ord (2nd β€˜π‘₯))
32 ordun 6422 . . . . . . . . 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 7681 . . . . . . . 8 ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ V
3635elon 6327 . . . . . . 7 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On ↔ Ord ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
3734, 36sylibr 233 . . . . . 6 (π‘₯ ∈ (On Γ— On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ On)
385, 37fmpti 7061 . . . . 5 (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On
3938a1i 11 . . . 4 (⊀ β†’ (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))):(On Γ— On)⟢On)
40 epweon 7710 . . . . 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 9952 . . . . 5 𝐿 We (On Γ— On)
4443a1i 11 . . . 4 (⊀ β†’ 𝐿 We (On Γ— On))
45 vex 3448 . . . . . . . 8 𝑒 ∈ V
4645dmex 7849 . . . . . . 7 dom 𝑒 ∈ V
4745rnex 7850 . . . . . . 7 ran 𝑒 ∈ V
4846, 47unex 7681 . . . . . 6 (dom 𝑒 βˆͺ ran 𝑒) ∈ V
49 imadmres 6187 . . . . . . 7 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒)) = ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒)
50 inss2 4190 . . . . . . . . . 10 (𝑒 ∩ (On Γ— On)) βŠ† (On Γ— On)
51 ssun1 4133 . . . . . . . . . . . . . 14 dom 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
52 elinel2 4157 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ (On Γ— On))
53 1st2nd2 7961 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (On Γ— On) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
5452, 53syl 17 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
55 elinel1 4156 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ π‘₯ ∈ 𝑒)
5654, 55eqeltrrd 2835 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒)
5728, 30opeldm 5864 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5856, 57syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ dom 𝑒)
5951, 58sselid 3943 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (1st β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
60 ssun2 4134 . . . . . . . . . . . . . 14 ran 𝑒 βŠ† (dom 𝑒 βˆͺ ran 𝑒)
6128, 30opelrn 5899 . . . . . . . . . . . . . . 15 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑒 β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6256, 61syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ ran 𝑒)
6360, 62sselid 3943 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ (2nd β€˜π‘₯) ∈ (dom 𝑒 βˆͺ ran 𝑒))
6459, 63prssd 4783 . . . . . . . . . . . 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 7762 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) ∈ On ∧ (2nd β€˜π‘₯) ∈ On) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6865, 66, 67syl2anc 585 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ {(1st β€˜π‘₯), (2nd β€˜π‘₯)})
6964, 68sseldd 3946 . . . . . . . . . . 11 (π‘₯ ∈ (𝑒 ∩ (On Γ— On)) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒))
7069rgen 3063 . . . . . . . . . 10 βˆ€π‘₯ ∈ (𝑒 ∩ (On Γ— On))((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)
71 ssrab 4031 . . . . . . . . . 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 5960 . . . . . . . . . 10 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))))
7438fdmi 6681 . . . . . . . . . . 11 dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) = (On Γ— On)
7574ineq2i 4170 . . . . . . . . . 10 (𝑒 ∩ dom (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))) = (𝑒 ∩ (On Γ— On))
7673, 75eqtri 2761 . . . . . . . . 9 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) = (𝑒 ∩ (On Γ— On))
775mptpreima 6191 . . . . . . . . 9 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒)) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ (dom 𝑒 βˆͺ ran 𝑒)}
7872, 76, 773sstr4i 3988 . . . . . . . 8 dom ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ (dom 𝑒 βˆͺ ran 𝑒))
79 funmpt 6540 . . . . . . . . 9 Fun (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
80 resss 5963 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β†Ύ 𝑒) βŠ† (π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)))
81 dmss 5859 . . . . . . . . . 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 7005 . . . . . . . . 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 3980 . . . . . 6 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (dom 𝑒 βˆͺ ran 𝑒)
8748, 86ssexi 5280 . . . . 5 ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
8887a1i 11 . . . 4 (⊀ β†’ ((π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
8925, 39, 41, 44, 88fnwe 8065 . . 3 (⊀ β†’ 𝑅 We (On Γ— On))
90 epse 5617 . . . . 5 E Se On
9190a1i 11 . . . 4 (⊀ β†’ E Se On)
92 vuniex 7677 . . . . . . . 8 βˆͺ 𝑒 ∈ V
9392pwex 5336 . . . . . . 7 𝒫 βˆͺ 𝑒 ∈ V
9493, 93xpex 7688 . . . . . 6 (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ∈ V
955mptpreima 6191 . . . . . . . 8 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) = {π‘₯ ∈ (On Γ— On) ∣ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒}
96 df-rab 3407 . . . . . . . 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 4899 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒 β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
10099adantl 483 . . . . . . . . . . . 12 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) βŠ† βˆͺ 𝑒)
101100unssad 4148 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
10228elpw 4565 . . . . . . . . . . 11 ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (1st β€˜π‘₯) βŠ† βˆͺ 𝑒)
103101, 102sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
104100unssbd 4149 . . . . . . . . . . 11 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
10530elpw 4565 . . . . . . . . . . 11 ((2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ↔ (2nd β€˜π‘₯) βŠ† βˆͺ 𝑒)
106104, 105sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)
107103, 106jca 513 . . . . . . . . 9 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒))
108 elxp6 7956 . . . . . . . . 9 (π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒) ↔ (π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∧ ((1st β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒 ∧ (2nd β€˜π‘₯) ∈ 𝒫 βˆͺ 𝑒)))
10998, 107, 108sylanbrc 584 . . . . . . . 8 ((π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒) β†’ π‘₯ ∈ (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒))
110109abssi 4028 . . . . . . 7 {π‘₯ ∣ (π‘₯ ∈ (On Γ— On) ∧ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯)) ∈ 𝑒)} βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11197, 110eqsstri 3979 . . . . . 6 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) βŠ† (𝒫 βˆͺ 𝑒 Γ— 𝒫 βˆͺ 𝑒)
11294, 111ssexi 5280 . . . . 5 (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V
113112a1i 11 . . . 4 (⊀ β†’ (β—‘(π‘₯ ∈ (On Γ— On) ↦ ((1st β€˜π‘₯) βˆͺ (2nd β€˜π‘₯))) β€œ 𝑒) ∈ V)
11425, 39, 91, 113fnse 8066 . . 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 3061  {crab 3406  Vcvv 3444   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911  π’« cpw 4561  {cpr 4589  βŸ¨cop 4593  βˆͺ cuni 4866   class class class wbr 5106  {copab 5168   ↦ cmpt 5189   E cep 5537   Se wse 5587   We wwe 5588   Γ— cxp 5632  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637  Ord word 6317  Oncon0 6318  Fun wfun 6491  βŸΆwf 6493  β€˜cfv 6497  1st c1st 7920  2nd c2nd 7921
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 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
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 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-1st 7922  df-2nd 7923
This theorem is referenced by:  infxpenlem  9954
  Copyright terms: Public domain W3C validator