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

Theorem r0weon 9025
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 6352 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (1st𝑥) = (1st𝑧))
3 fveq2 6352 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (2nd𝑥) = (2nd𝑧))
42, 3uneq12d 3911 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((1st𝑥) ∪ (2nd𝑥)) = ((1st𝑧) ∪ (2nd𝑧)))
5 eqid 2760 . . . . . . . . . . 11 (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) = (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))
6 fvex 6362 . . . . . . . . . . . 12 (1st𝑧) ∈ V
7 fvex 6362 . . . . . . . . . . . 12 (2nd𝑧) ∈ V
86, 7unex 7121 . . . . . . . . . . 11 ((1st𝑧) ∪ (2nd𝑧)) ∈ V
94, 5, 8fvmpt 6444 . . . . . . . . . 10 (𝑧 ∈ (On × On) → ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) = ((1st𝑧) ∪ (2nd𝑧)))
10 fveq2 6352 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
11 fveq2 6352 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
1210, 11uneq12d 3911 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((1st𝑥) ∪ (2nd𝑥)) = ((1st𝑤) ∪ (2nd𝑤)))
13 fvex 6362 . . . . . . . . . . . 12 (1st𝑤) ∈ V
14 fvex 6362 . . . . . . . . . . . 12 (2nd𝑤) ∈ V
1513, 14unex 7121 . . . . . . . . . . 11 ((1st𝑤) ∪ (2nd𝑤)) ∈ V
1612, 5, 15fvmpt 6444 . . . . . . . . . 10 (𝑤 ∈ (On × On) → ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) = ((1st𝑤) ∪ (2nd𝑤)))
179, 16breqan12d 4820 . . . . . . . . 9 ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) → (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ↔ ((1st𝑧) ∪ (2nd𝑧)) E ((1st𝑤) ∪ (2nd𝑤))))
1815epelc 5181 . . . . . . . . 9 (((1st𝑧) ∪ (2nd𝑧)) E ((1st𝑤) ∪ (2nd𝑤)) ↔ ((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)))
1917, 18syl6bb 276 . . . . . . . 8 ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) → (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ↔ ((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤))))
209, 16eqeqan12d 2776 . . . . . . . . 9 ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) → (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ↔ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
2120anbi1d 743 . . . . . . . 8 ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) → ((((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤) ↔ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))
2219, 21orbi12d 748 . . . . . . 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 672 . . . . . 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 4869 . . . . 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 2785 . . . 4 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))}
26 xp1st 7365 . . . . . . . 8 (𝑥 ∈ (On × On) → (1st𝑥) ∈ On)
27 xp2nd 7366 . . . . . . . 8 (𝑥 ∈ (On × On) → (2nd𝑥) ∈ On)
28 fvex 6362 . . . . . . . . . 10 (1st𝑥) ∈ V
2928elon 5893 . . . . . . . . 9 ((1st𝑥) ∈ On ↔ Ord (1st𝑥))
30 fvex 6362 . . . . . . . . . 10 (2nd𝑥) ∈ V
3130elon 5893 . . . . . . . . 9 ((2nd𝑥) ∈ On ↔ Ord (2nd𝑥))
32 ordun 5990 . . . . . . . . 9 ((Ord (1st𝑥) ∧ Ord (2nd𝑥)) → Ord ((1st𝑥) ∪ (2nd𝑥)))
3329, 31, 32syl2anb 497 . . . . . . . 8 (((1st𝑥) ∈ On ∧ (2nd𝑥) ∈ On) → Ord ((1st𝑥) ∪ (2nd𝑥)))
3426, 27, 33syl2anc 696 . . . . . . 7 (𝑥 ∈ (On × On) → Ord ((1st𝑥) ∪ (2nd𝑥)))
3528, 30unex 7121 . . . . . . . 8 ((1st𝑥) ∪ (2nd𝑥)) ∈ V
3635elon 5893 . . . . . . 7 (((1st𝑥) ∪ (2nd𝑥)) ∈ On ↔ Ord ((1st𝑥) ∪ (2nd𝑥)))
3734, 36sylibr 224 . . . . . 6 (𝑥 ∈ (On × On) → ((1st𝑥) ∪ (2nd𝑥)) ∈ On)
385, 37fmpti 6546 . . . . 5 (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))):(On × On)⟶On
3938a1i 11 . . . 4 (⊤ → (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))):(On × On)⟶On)
40 epweon 7148 . . . . 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 9024 . . . . 5 𝐿 We (On × On)
4443a1i 11 . . . 4 (⊤ → 𝐿 We (On × On))
45 vex 3343 . . . . . . . 8 𝑢 ∈ V
4645dmex 7264 . . . . . . 7 dom 𝑢 ∈ V
4745rnex 7265 . . . . . . 7 ran 𝑢 ∈ V
4846, 47unex 7121 . . . . . 6 (dom 𝑢 ∪ ran 𝑢) ∈ V
49 imadmres 5788 . . . . . . 7 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢)) = ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢)
50 inss2 3977 . . . . . . . . . 10 (𝑢 ∩ (On × On)) ⊆ (On × On)
51 ssun1 3919 . . . . . . . . . . . . . 14 dom 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢)
5250sseli 3740 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ (On × On))
53 1st2nd2 7372 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (On × On) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
5452, 53syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
55 inss1 3976 . . . . . . . . . . . . . . . . 17 (𝑢 ∩ (On × On)) ⊆ 𝑢
5655sseli 3740 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥𝑢)
5754, 56eqeltrrd 2840 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑢 ∩ (On × On)) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑢)
5828, 30opeldm 5483 . . . . . . . . . . . . . . 15 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑢 → (1st𝑥) ∈ dom 𝑢)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑢 ∩ (On × On)) → (1st𝑥) ∈ dom 𝑢)
6051, 59sseldi 3742 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (On × On)) → (1st𝑥) ∈ (dom 𝑢 ∪ ran 𝑢))
61 ssun2 3920 . . . . . . . . . . . . . 14 ran 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢)
6228, 30opelrn 5512 . . . . . . . . . . . . . . 15 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑢 → (2nd𝑥) ∈ ran 𝑢)
6357, 62syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑢 ∩ (On × On)) → (2nd𝑥) ∈ ran 𝑢)
6461, 63sseldi 3742 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (On × On)) → (2nd𝑥) ∈ (dom 𝑢 ∪ ran 𝑢))
65 prssi 4498 . . . . . . . . . . . . 13 (((1st𝑥) ∈ (dom 𝑢 ∪ ran 𝑢) ∧ (2nd𝑥) ∈ (dom 𝑢 ∪ ran 𝑢)) → {(1st𝑥), (2nd𝑥)} ⊆ (dom 𝑢 ∪ ran 𝑢))
6660, 64, 65syl2anc 696 . . . . . . . . . . . 12 (𝑥 ∈ (𝑢 ∩ (On × On)) → {(1st𝑥), (2nd𝑥)} ⊆ (dom 𝑢 ∪ ran 𝑢))
6752, 26syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (On × On)) → (1st𝑥) ∈ On)
6852, 27syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (On × On)) → (2nd𝑥) ∈ On)
69 ordunpr 7191 . . . . . . . . . . . . 13 (((1st𝑥) ∈ On ∧ (2nd𝑥) ∈ On) → ((1st𝑥) ∪ (2nd𝑥)) ∈ {(1st𝑥), (2nd𝑥)})
7067, 68, 69syl2anc 696 . . . . . . . . . . . 12 (𝑥 ∈ (𝑢 ∩ (On × On)) → ((1st𝑥) ∪ (2nd𝑥)) ∈ {(1st𝑥), (2nd𝑥)})
7166, 70sseldd 3745 . . . . . . . . . . 11 (𝑥 ∈ (𝑢 ∩ (On × On)) → ((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢))
7271rgen 3060 . . . . . . . . . 10 𝑥 ∈ (𝑢 ∩ (On × On))((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)
73 ssrab 3821 . . . . . . . . . 10 ((𝑢 ∩ (On × On)) ⊆ {𝑥 ∈ (On × On) ∣ ((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} ↔ ((𝑢 ∩ (On × On)) ⊆ (On × On) ∧ ∀𝑥 ∈ (𝑢 ∩ (On × On))((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)))
7450, 72, 73mpbir2an 993 . . . . . . . . 9 (𝑢 ∩ (On × On)) ⊆ {𝑥 ∈ (On × On) ∣ ((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)}
75 dmres 5577 . . . . . . . . . 10 dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) = (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))))
7638fdmi 6213 . . . . . . . . . . 11 dom (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) = (On × On)
7776ineq2i 3954 . . . . . . . . . 10 (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))) = (𝑢 ∩ (On × On))
7875, 77eqtri 2782 . . . . . . . . 9 dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) = (𝑢 ∩ (On × On))
795mptpreima 5789 . . . . . . . . 9 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) = {𝑥 ∈ (On × On) ∣ ((1st𝑥) ∪ (2nd𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)}
8074, 78, 793sstr4i 3785 . . . . . . . 8 dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ (dom 𝑢 ∪ ran 𝑢))
81 funmpt 6087 . . . . . . . . 9 Fun (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))
82 resss 5580 . . . . . . . . . 10 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))
83 dmss 5478 . . . . . . . . . 10 (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) → dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))))
8482, 83ax-mp 5 . . . . . . . . 9 dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥)))
85 funimass3 6496 . . . . . . . . 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 𝑢))))
8681, 84, 85mp2an 710 . . . . . . . 8 (((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢) ⊆ ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ (dom 𝑢 ∪ ran 𝑢)))
8780, 86mpbir 221 . . . . . . 7 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ dom ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢)
8849, 87eqsstr3i 3777 . . . . . 6 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ⊆ (dom 𝑢 ∪ ran 𝑢)
8948, 88ssexi 4955 . . . . 5 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ∈ V
9089a1i 11 . . . 4 (⊤ → ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ∈ V)
9125, 39, 41, 44, 90fnwe 7461 . . 3 (⊤ → 𝑅 We (On × On))
92 epse 5249 . . . . 5 E Se On
9392a1i 11 . . . 4 (⊤ → E Se On)
94 vuniex 7119 . . . . . . . 8 𝑢 ∈ V
9594pwex 4997 . . . . . . 7 𝒫 𝑢 ∈ V
9695, 95xpex 7127 . . . . . 6 (𝒫 𝑢 × 𝒫 𝑢) ∈ V
975mptpreima 5789 . . . . . . . 8 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) = {𝑥 ∈ (On × On) ∣ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢}
98 df-rab 3059 . . . . . . . 8 {𝑥 ∈ (On × On) ∣ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢} = {𝑥 ∣ (𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢)}
9997, 98eqtri 2782 . . . . . . 7 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) = {𝑥 ∣ (𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢)}
10053adantr 472 . . . . . . . . 9 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
101 elssuni 4619 . . . . . . . . . . . . 13 (((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢 → ((1st𝑥) ∪ (2nd𝑥)) ⊆ 𝑢)
102101adantl 473 . . . . . . . . . . . 12 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → ((1st𝑥) ∪ (2nd𝑥)) ⊆ 𝑢)
103102unssad 3933 . . . . . . . . . . 11 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → (1st𝑥) ⊆ 𝑢)
10428elpw 4308 . . . . . . . . . . 11 ((1st𝑥) ∈ 𝒫 𝑢 ↔ (1st𝑥) ⊆ 𝑢)
105103, 104sylibr 224 . . . . . . . . . 10 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → (1st𝑥) ∈ 𝒫 𝑢)
106102unssbd 3934 . . . . . . . . . . 11 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → (2nd𝑥) ⊆ 𝑢)
10730elpw 4308 . . . . . . . . . . 11 ((2nd𝑥) ∈ 𝒫 𝑢 ↔ (2nd𝑥) ⊆ 𝑢)
108106, 107sylibr 224 . . . . . . . . . 10 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → (2nd𝑥) ∈ 𝒫 𝑢)
109105, 108jca 555 . . . . . . . . 9 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → ((1st𝑥) ∈ 𝒫 𝑢 ∧ (2nd𝑥) ∈ 𝒫 𝑢))
110 elxp6 7367 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑢 × 𝒫 𝑢) ↔ (𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩ ∧ ((1st𝑥) ∈ 𝒫 𝑢 ∧ (2nd𝑥) ∈ 𝒫 𝑢)))
111100, 109, 110sylanbrc 701 . . . . . . . 8 ((𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢) → 𝑥 ∈ (𝒫 𝑢 × 𝒫 𝑢))
112111abssi 3818 . . . . . . 7 {𝑥 ∣ (𝑥 ∈ (On × On) ∧ ((1st𝑥) ∪ (2nd𝑥)) ∈ 𝑢)} ⊆ (𝒫 𝑢 × 𝒫 𝑢)
11399, 112eqsstri 3776 . . . . . 6 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ⊆ (𝒫 𝑢 × 𝒫 𝑢)
11496, 113ssexi 4955 . . . . 5 ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ∈ V
115114a1i 11 . . . 4 (⊤ → ((𝑥 ∈ (On × On) ↦ ((1st𝑥) ∪ (2nd𝑥))) “ 𝑢) ∈ V)
11625, 39, 93, 115fnse 7462 . . 3 (⊤ → 𝑅 Se (On × On))
11791, 116jca 555 . 2 (⊤ → (𝑅 We (On × On) ∧ 𝑅 Se (On × On)))
118117trud 1642 1 (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382  wa 383   = wceq 1632  wtru 1633  wcel 2139  {cab 2746  wral 3050  {crab 3054  Vcvv 3340  cun 3713  cin 3714  wss 3715  𝒫 cpw 4302  {cpr 4323  cop 4327   cuni 4588   class class class wbr 4804  {copab 4864  cmpt 4881   E cep 5178   Se wse 5223   We wwe 5224   × cxp 5264  ccnv 5265  dom cdm 5266  ran crn 5267  cres 5268  cima 5269  Ord word 5883  Oncon0 5884  Fun wfun 6043  wf 6045  cfv 6049  1st c1st 7331  2nd c2nd 7332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-ord 5887  df-on 5888  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-1st 7333  df-2nd 7334
This theorem is referenced by:  infxpenlem  9026
  Copyright terms: Public domain W3C validator