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

Theorem inar1 9879
Description: (𝑅1𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.)
Assertion
Ref Expression
inar1 (𝐴 ∈ Inacc → (𝑅1𝐴) ≈ 𝐴)

Proof of Theorem inar1
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inawina 9794 . . . . . 6 (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2 winaon 9792 . . . . . 6 (𝐴 ∈ Inaccw𝐴 ∈ On)
31, 2syl 17 . . . . 5 (𝐴 ∈ Inacc → 𝐴 ∈ On)
4 winalim 9799 . . . . . 6 (𝐴 ∈ Inaccw → Lim 𝐴)
51, 4syl 17 . . . . 5 (𝐴 ∈ Inacc → Lim 𝐴)
6 r1lim 8879 . . . . 5 ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
73, 5, 6syl2anc 575 . . . 4 (𝐴 ∈ Inacc → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
8 onelon 5958 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑥𝐴) → 𝑥 ∈ On)
93, 8sylan 571 . . . . . . . 8 ((𝐴 ∈ Inacc ∧ 𝑥𝐴) → 𝑥 ∈ On)
10 eleq1 2872 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ∈ 𝐴))
11 fveq2 6405 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑅1𝑥) = (𝑅1‘∅))
1211breq1d 4850 . . . . . . . . . . 11 (𝑥 = ∅ → ((𝑅1𝑥) ≺ 𝐴 ↔ (𝑅1‘∅) ≺ 𝐴))
1310, 12imbi12d 335 . . . . . . . . . 10 (𝑥 = ∅ → ((𝑥𝐴 → (𝑅1𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴)))
14 eleq1 2872 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
15 fveq2 6405 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
1615breq1d 4850 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑅1𝑥) ≺ 𝐴 ↔ (𝑅1𝑦) ≺ 𝐴))
1714, 16imbi12d 335 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝑅1𝑥) ≺ 𝐴) ↔ (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴)))
18 eleq1 2872 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑥𝐴 ↔ suc 𝑦𝐴))
19 fveq2 6405 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
2019breq1d 4850 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑅1𝑥) ≺ 𝐴 ↔ (𝑅1‘suc 𝑦) ≺ 𝐴))
2118, 20imbi12d 335 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑥𝐴 → (𝑅1𝑥) ≺ 𝐴) ↔ (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
22 ne0i 4119 . . . . . . . . . . . . 13 (∅ ∈ 𝐴𝐴 ≠ ∅)
23 0sdomg 8325 . . . . . . . . . . . . 13 (𝐴 ∈ On → (∅ ≺ 𝐴𝐴 ≠ ∅))
2422, 23syl5ibr 237 . . . . . . . . . . . 12 (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ≺ 𝐴))
25 r10 8875 . . . . . . . . . . . . 13 (𝑅1‘∅) = ∅
2625breq1i 4847 . . . . . . . . . . . 12 ((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴)
2724, 26syl6ibr 243 . . . . . . . . . . 11 (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
281, 2, 273syl 18 . . . . . . . . . 10 (𝐴 ∈ Inacc → (∅ ∈ 𝐴 → (𝑅1‘∅) ≺ 𝐴))
29 eloni 5943 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → Ord 𝐴)
30 ordtr 5947 . . . . . . . . . . . . . . 15 (Ord 𝐴 → Tr 𝐴)
3129, 30syl 17 . . . . . . . . . . . . . 14 (𝐴 ∈ On → Tr 𝐴)
32 trsuc 6020 . . . . . . . . . . . . . . 15 ((Tr 𝐴 ∧ suc 𝑦𝐴) → 𝑦𝐴)
3332ex 399 . . . . . . . . . . . . . 14 (Tr 𝐴 → (suc 𝑦𝐴𝑦𝐴))
343, 31, 333syl 18 . . . . . . . . . . . . 13 (𝐴 ∈ Inacc → (suc 𝑦𝐴𝑦𝐴))
3534adantl 469 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦𝐴𝑦𝐴))
36 r1suc 8877 . . . . . . . . . . . . . . 15 (𝑦 ∈ On → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1𝑦))
37 fvex 6418 . . . . . . . . . . . . . . . . . 18 (𝑅1𝑦) ∈ V
3837cardid 9651 . . . . . . . . . . . . . . . . 17 (card‘(𝑅1𝑦)) ≈ (𝑅1𝑦)
3938ensymi 8239 . . . . . . . . . . . . . . . 16 (𝑅1𝑦) ≈ (card‘(𝑅1𝑦))
40 pwen 8369 . . . . . . . . . . . . . . . 16 ((𝑅1𝑦) ≈ (card‘(𝑅1𝑦)) → 𝒫 (𝑅1𝑦) ≈ 𝒫 (card‘(𝑅1𝑦)))
4139, 40ax-mp 5 . . . . . . . . . . . . . . 15 𝒫 (𝑅1𝑦) ≈ 𝒫 (card‘(𝑅1𝑦))
4236, 41syl6eqbr 4879 . . . . . . . . . . . . . 14 (𝑦 ∈ On → (𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1𝑦)))
43 winacard 9796 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
4443eleq2d 2870 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ Inaccw → ((card‘(𝑅1𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1𝑦)) ∈ 𝐴))
45 cardsdom 9659 . . . . . . . . . . . . . . . . . . 19 (((𝑅1𝑦) ∈ V ∧ 𝐴 ∈ On) → ((card‘(𝑅1𝑦)) ∈ (card‘𝐴) ↔ (𝑅1𝑦) ≺ 𝐴))
4637, 2, 45sylancr 577 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ Inaccw → ((card‘(𝑅1𝑦)) ∈ (card‘𝐴) ↔ (𝑅1𝑦) ≺ 𝐴))
4744, 46bitr3d 272 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Inaccw → ((card‘(𝑅1𝑦)) ∈ 𝐴 ↔ (𝑅1𝑦) ≺ 𝐴))
481, 47syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Inacc → ((card‘(𝑅1𝑦)) ∈ 𝐴 ↔ (𝑅1𝑦) ≺ 𝐴))
49 elina 9791 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧𝐴 𝒫 𝑧𝐴))
5049simp3bi 1170 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Inacc → ∀𝑧𝐴 𝒫 𝑧𝐴)
51 pweq 4351 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (card‘(𝑅1𝑦)) → 𝒫 𝑧 = 𝒫 (card‘(𝑅1𝑦)))
5251breq1d 4850 . . . . . . . . . . . . . . . . . 18 (𝑧 = (card‘(𝑅1𝑦)) → (𝒫 𝑧𝐴 ↔ 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴))
5352rspccv 3498 . . . . . . . . . . . . . . . . 17 (∀𝑧𝐴 𝒫 𝑧𝐴 → ((card‘(𝑅1𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴))
5450, 53syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Inacc → ((card‘(𝑅1𝑦)) ∈ 𝐴 → 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴))
5548, 54sylbird 251 . . . . . . . . . . . . . . 15 (𝐴 ∈ Inacc → ((𝑅1𝑦) ≺ 𝐴 → 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴))
5655imp 395 . . . . . . . . . . . . . 14 ((𝐴 ∈ Inacc ∧ (𝑅1𝑦) ≺ 𝐴) → 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴)
57 ensdomtr 8332 . . . . . . . . . . . . . 14 (((𝑅1‘suc 𝑦) ≈ 𝒫 (card‘(𝑅1𝑦)) ∧ 𝒫 (card‘(𝑅1𝑦)) ≺ 𝐴) → (𝑅1‘suc 𝑦) ≺ 𝐴)
5842, 56, 57syl2an 585 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧ (𝑅1𝑦) ≺ 𝐴)) → (𝑅1‘suc 𝑦) ≺ 𝐴)
5958expr 446 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑅1𝑦) ≺ 𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))
6035, 59imim12d 81 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴)))
6160ex 399 . . . . . . . . . 10 (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ≺ 𝐴))))
62 vex 3393 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
63 r1lim 8879 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ∧ Lim 𝑥) → (𝑅1𝑥) = 𝑧𝑥 (𝑅1𝑧))
6462, 63mpan 673 . . . . . . . . . . . . . . 15 (Lim 𝑥 → (𝑅1𝑥) = 𝑧𝑥 (𝑅1𝑧))
65 nfcv 2947 . . . . . . . . . . . . . . . . . . 19 𝑦𝑧
66 nfcv 2947 . . . . . . . . . . . . . . . . . . . 20 𝑦(𝑅1𝑧)
67 nfcv 2947 . . . . . . . . . . . . . . . . . . . 20 𝑦
68 nfiu1 4738 . . . . . . . . . . . . . . . . . . . 20 𝑦 𝑦𝑥 (card‘(𝑅1𝑦))
6966, 67, 68nfbr 4887 . . . . . . . . . . . . . . . . . . 19 𝑦(𝑅1𝑧) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))
70 fveq2 6405 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (𝑅1𝑦) = (𝑅1𝑧))
7170breq1d 4850 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → ((𝑅1𝑦) ≼ 𝑦𝑥 (card‘(𝑅1𝑦)) ↔ (𝑅1𝑧) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))))
72 fvex 6418 . . . . . . . . . . . . . . . . . . . . . 22 (card‘(𝑅1𝑦)) ∈ V
7362, 72iunex 7374 . . . . . . . . . . . . . . . . . . . . 21 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ V
74 ssiun2 4751 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑥 → (card‘(𝑅1𝑦)) ⊆ 𝑦𝑥 (card‘(𝑅1𝑦)))
75 ssdomg 8235 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ V → ((card‘(𝑅1𝑦)) ⊆ 𝑦𝑥 (card‘(𝑅1𝑦)) → (card‘(𝑅1𝑦)) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))))
7673, 74, 75mpsyl 68 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑥 → (card‘(𝑅1𝑦)) ≼ 𝑦𝑥 (card‘(𝑅1𝑦)))
77 endomtr 8247 . . . . . . . . . . . . . . . . . . . 20 (((𝑅1𝑦) ≈ (card‘(𝑅1𝑦)) ∧ (card‘(𝑅1𝑦)) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝑅1𝑦) ≼ 𝑦𝑥 (card‘(𝑅1𝑦)))
7839, 76, 77sylancr 577 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑥 → (𝑅1𝑦) ≼ 𝑦𝑥 (card‘(𝑅1𝑦)))
7965, 69, 71, 78vtoclgaf 3463 . . . . . . . . . . . . . . . . . 18 (𝑧𝑥 → (𝑅1𝑧) ≼ 𝑦𝑥 (card‘(𝑅1𝑦)))
8079rgen 3109 . . . . . . . . . . . . . . . . 17 𝑧𝑥 (𝑅1𝑧) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))
81 iundom 9646 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ V ∧ ∀𝑧𝑥 (𝑅1𝑧) ≼ 𝑦𝑥 (card‘(𝑅1𝑦))) → 𝑧𝑥 (𝑅1𝑧) ≼ (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))))
8262, 80, 81mp2an 675 . . . . . . . . . . . . . . . 16 𝑧𝑥 (𝑅1𝑧) ≼ (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦)))
8362, 73unex 7183 . . . . . . . . . . . . . . . . . . . 20 (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ V
84 ssun2 3973 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))
85 ssdomg 8235 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ V → ( 𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → 𝑦𝑥 (card‘(𝑅1𝑦)) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
8683, 84, 85mp2 9 . . . . . . . . . . . . . . . . . . 19 𝑦𝑥 (card‘(𝑅1𝑦)) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))
8762xpdom2 8291 . . . . . . . . . . . . . . . . . . 19 ( 𝑦𝑥 (card‘(𝑅1𝑦)) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
89 ssun1 3972 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))
90 ssdomg 8235 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ V → (𝑥 ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → 𝑥 ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
9183, 89, 90mp2 9 . . . . . . . . . . . . . . . . . . 19 𝑥 ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))
9283xpdom1 8295 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
94 domtr 8242 . . . . . . . . . . . . . . . . . 18 (((𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ∧ (𝑥 × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))) → (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
9588, 93, 94mp2an 675 . . . . . . . . . . . . . . . . 17 (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
96 limomss 7297 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝑥 → ω ⊆ 𝑥)
9796, 89syl6ss 3807 . . . . . . . . . . . . . . . . . . 19 (Lim 𝑥 → ω ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
98 ssdomg 8235 . . . . . . . . . . . . . . . . . . 19 ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ V → (ω ⊆ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → ω ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))))
9983, 97, 98mpsyl 68 . . . . . . . . . . . . . . . . . 18 (Lim 𝑥 → ω ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
100 infxpidm 9666 . . . . . . . . . . . . . . . . . 18 (ω ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≈ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
10199, 100syl 17 . . . . . . . . . . . . . . . . 17 (Lim 𝑥 → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≈ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
102 domentr 8248 . . . . . . . . . . . . . . . . 17 (((𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ∧ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) × (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) ≈ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) → (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
10395, 101, 102sylancr 577 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
104 domtr 8242 . . . . . . . . . . . . . . . 16 (( 𝑧𝑥 (𝑅1𝑧) ≼ (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ∧ (𝑥 × 𝑦𝑥 (card‘(𝑅1𝑦))) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦)))) → 𝑧𝑥 (𝑅1𝑧) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
10582, 103, 104sylancr 577 . . . . . . . . . . . . . . 15 (Lim 𝑥 𝑧𝑥 (𝑅1𝑧) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
10664, 105eqbrtrd 4862 . . . . . . . . . . . . . 14 (Lim 𝑥 → (𝑅1𝑥) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
107106ad2antlr 709 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝑅1𝑥) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
108 eleq1a 2879 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → (𝐴 = 𝑥𝐴𝐴))
109 ordirr 5951 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴 → ¬ 𝐴𝐴)
1103, 29, 1093syl 18 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Inacc → ¬ 𝐴𝐴)
111108, 110nsyli 156 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥))
112111imp 395 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥)
113112ad2ant2r 744 . . . . . . . . . . . . . . . 16 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥)
114 simpll 774 . . . . . . . . . . . . . . . . 17 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → 𝑥𝐴)
115 limord 5994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim 𝑥 → Ord 𝑥)
11662elon 5942 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ On ↔ Ord 𝑥)
117115, 116sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑥𝑥 ∈ On)
118117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → 𝑥 ∈ On)
119 cardf 9654 . . . . . . . . . . . . . . . . . . . . . . . . 25 card:V⟶On
120 r1fnon 8874 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑅1 Fn On
121 dffn2 6255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅1 Fn On ↔ 𝑅1:On⟶V)
122120, 121mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅1:On⟶V
123 fco 6270 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((card:V⟶On ∧ 𝑅1:On⟶V) → (card ∘ 𝑅1):On⟶On)
124119, 122, 123mp2an 675 . . . . . . . . . . . . . . . . . . . . . . . 24 (card ∘ 𝑅1):On⟶On
125 onss 7217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ On → 𝑥 ⊆ On)
126 fssres 6282 . . . . . . . . . . . . . . . . . . . . . . . 24 (((card ∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
127124, 125, 126sylancr 577 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ On → ((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On)
128 ffn 6253 . . . . . . . . . . . . . . . . . . . . . . 23 (((card ∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
129118, 127, 1283syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥)
1303ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → 𝐴 ∈ On)
131 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → 𝑦𝑥)
132 simplll 782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → 𝑥𝐴)
133 ontr1 5981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∈ On → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
134133imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (𝑦𝑥𝑥𝐴)) → 𝑦𝐴)
135130, 131, 132, 134syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → 𝑦𝐴)
13637, 130, 45sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((card‘(𝑅1𝑦)) ∈ (card‘𝐴) ↔ (𝑅1𝑦) ≺ 𝐴))
1371, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴 ∈ Inacc → (card‘𝐴) = 𝐴)
138137ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → (card‘𝐴) = 𝐴)
139138eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((card‘(𝑅1𝑦)) ∈ (card‘𝐴) ↔ (card‘(𝑅1𝑦)) ∈ 𝐴))
140136, 139bitr3d 272 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((𝑅1𝑦) ≺ 𝐴 ↔ (card‘(𝑅1𝑦)) ∈ 𝐴))
141140biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((𝑅1𝑦) ≺ 𝐴 → (card‘(𝑅1𝑦)) ∈ 𝐴))
142135, 141embantd 59 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (card‘(𝑅1𝑦)) ∈ 𝐴))
143117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On)
144 fvres 6424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝑥 → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
145144adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ 𝑦𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘ 𝑅1)‘𝑦))
146 onelon 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
147 fvco3 6493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
148122, 146, 147sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
149145, 148eqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ On ∧ 𝑦𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1𝑦)))
150143, 149sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) = (card‘(𝑅1𝑦)))
151150eleq1d 2869 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔ (card‘(𝑅1𝑦)) ∈ 𝐴))
152142, 151sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
153152ralimdva 3149 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → ∀𝑦𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
154153impr 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ∀𝑦𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)
155 ffnfv 6607 . . . . . . . . . . . . . . . . . . . . . 22 (((card ∘ 𝑅1) ↾ 𝑥):𝑥𝐴 ↔ (((card ∘ 𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦𝑥 (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴))
156129, 154, 155sylanbrc 574 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((card ∘ 𝑅1) ↾ 𝑥):𝑥𝐴)
157 eleq2 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → (𝑧𝐴𝑧 𝑦𝑥 (card‘(𝑅1𝑦))))
158157biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) ∧ 𝑧𝐴) → 𝑧 𝑦𝑥 (card‘(𝑅1𝑦)))
159 eliun 4712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 𝑦𝑥 (card‘(𝑅1𝑦)) ↔ ∃𝑦𝑥 𝑧 ∈ (card‘(𝑅1𝑦)))
160 cardon 9050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (card‘(𝑅1𝑦)) ∈ On
161160onelssi 6046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (card‘(𝑅1𝑦)) → 𝑧 ⊆ (card‘(𝑅1𝑦)))
162149sseq2d 3827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆ (card‘(𝑅1𝑦))))
163161, 162syl5ibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑧 ∈ (card‘(𝑅1𝑦)) → 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
164163reximdva 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ On → (∃𝑦𝑥 𝑧 ∈ (card‘(𝑅1𝑦)) → ∃𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
165159, 164syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ On → (𝑧 𝑦𝑥 (card‘(𝑅1𝑦)) → ∃𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
166158, 165syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ On → ((𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) ∧ 𝑧𝐴) → ∃𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
167166expdimp 442 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ On ∧ 𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝑧𝐴 → ∃𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
168167ralrimiv 3152 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ On ∧ 𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦))) → ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
169168ex 399 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ On → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
170118, 169syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
171 ffun 6256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((card ∘ 𝑅1):On⟶On → Fun (card ∘ 𝑅1))
172124, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (card ∘ 𝑅1)
173 resfunexg 6701 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun (card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘ 𝑅1) ↾ 𝑥) ∈ V)
174172, 62, 173mp2an 675 . . . . . . . . . . . . . . . . . . . . . 22 ((card ∘ 𝑅1) ↾ 𝑥) ∈ V
175 feq1 6234 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤:𝑥𝐴 ↔ ((card ∘ 𝑅1) ↾ 𝑥):𝑥𝐴))
176 fveq1 6404 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑤𝑦) = (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))
177176sseq2d 3827 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤𝑦) ↔ 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
178177rexbidv 3239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∃𝑦𝑥 𝑧 ⊆ (𝑤𝑦) ↔ ∃𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
179178ralbidv 3173 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → (∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦) ↔ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)))
180175, 179anbi12d 618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ((card ∘ 𝑅1) ↾ 𝑥) → ((𝑤:𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦)) ↔ (((card ∘ 𝑅1) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦))))
181174, 180spcev 3492 . . . . . . . . . . . . . . . . . . . . 21 ((((card ∘ 𝑅1) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (((card ∘ 𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦)))
182156, 170, 181syl6an 666 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → ∃𝑤(𝑤:𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦))))
1833ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → 𝐴 ∈ On)
184 cfflb 9363 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦)) → (cf‘𝐴) ⊆ 𝑥))
185183, 118, 184syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (∃𝑤(𝑤:𝑥𝐴 ∧ ∀𝑧𝐴𝑦𝑥 𝑧 ⊆ (𝑤𝑦)) → (cf‘𝐴) ⊆ 𝑥))
186182, 185syld 47 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → (cf‘𝐴) ⊆ 𝑥))
18749simp2bi 1169 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
188187sseq1d 3826 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ Inacc → ((cf‘𝐴) ⊆ 𝑥𝐴𝑥))
189188ad2antrl 710 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥𝐴𝑥))
190186, 189sylibd 230 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → 𝐴𝑥))
191 ontri1 5967 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴𝑥 ↔ ¬ 𝑥𝐴))
192183, 118, 191syl2anc 575 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴𝑥 ↔ ¬ 𝑥𝐴))
193190, 192sylibd 230 . . . . . . . . . . . . . . . . 17 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)) → ¬ 𝑥𝐴))
194114, 193mt2d 133 . . . . . . . . . . . . . . . 16 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)))
195 iunon 7669 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On) → 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On)
19662, 195mpan 673 . . . . . . . . . . . . . . . . . 18 (∀𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On → 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On)
197160a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦𝑥 → (card‘(𝑅1𝑦)) ∈ On)
198196, 197mprg 3113 . . . . . . . . . . . . . . . . 17 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On
199 eqcom 2812 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴𝐴 = (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))))
200 eloni 5943 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ On → Ord 𝑥)
201 eloni 5943 . . . . . . . . . . . . . . . . . . 19 ( 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On → Ord 𝑦𝑥 (card‘(𝑅1𝑦)))
202 ordequn 6038 . . . . . . . . . . . . . . . . . . 19 ((Ord 𝑥 ∧ Ord 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝐴 = (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝐴 = 𝑥𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)))))
203200, 201, 202syl2an 585 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ On ∧ 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On) → (𝐴 = (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝐴 = 𝑥𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)))))
204199, 203syl5bi 233 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝑦𝑥 (card‘(𝑅1𝑦)) ∈ On) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴 → (𝐴 = 𝑥𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)))))
205118, 198, 204sylancl 576 . . . . . . . . . . . . . . . 16 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴 → (𝐴 = 𝑥𝐴 = 𝑦𝑥 (card‘(𝑅1𝑦)))))
206113, 194, 205mtord 895 . . . . . . . . . . . . . . 15 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ¬ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴)
207 onelss 5976 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ On → (𝑥𝐴𝑥𝐴))
208183, 114, 207sylc 65 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → 𝑥𝐴)
209 onelss 5976 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ On → ((card‘(𝑅1𝑦)) ∈ 𝐴 → (card‘(𝑅1𝑦)) ⊆ 𝐴))
210130, 142, 209sylsyld 61 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (card‘(𝑅1𝑦)) ⊆ 𝐴))
211210ralimdva 3149 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → ∀𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ 𝐴))
212211impr 444 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ∀𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ 𝐴)
213 iunss 4749 . . . . . . . . . . . . . . . . . . . 20 ( 𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ 𝐴 ↔ ∀𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ 𝐴)
214212, 213sylibr 225 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → 𝑦𝑥 (card‘(𝑅1𝑦)) ⊆ 𝐴)
215208, 214unssd 3985 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ⊆ 𝐴)
216 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅))
217 iuneq1 4722 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑦𝑥 (card‘(𝑅1𝑦)) = 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)))
218216, 217uneq12d 3964 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦))))
219218eleq1d 2869 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦))) ∈ On))
220 0elon 5988 . . . . . . . . . . . . . . . . . . . . . . . 24 ∅ ∈ On
221220elimel 4343 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ∈ On, 𝑥, ∅) ∈ On
222221elexi 3406 . . . . . . . . . . . . . . . . . . . . . . . . 25 if(𝑥 ∈ On, 𝑥, ∅) ∈ V
223 iunon 7669 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((if(𝑥 ∈ On, 𝑥, ∅) ∈ V ∧ ∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)) ∈ On) → 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)) ∈ On)
224222, 223mpan 673 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)) ∈ On → 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)) ∈ On)
225160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ if(𝑥 ∈ On, 𝑥, ∅) → (card‘(𝑅1𝑦)) ∈ On)
226224, 225mprg 3113 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦)) ∈ On
227221, 226onun2i 6053 . . . . . . . . . . . . . . . . . . . . . 22 (if(𝑥 ∈ On, 𝑥, ∅) ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥, ∅)(card‘(𝑅1𝑦))) ∈ On
228219, 227dedth 4332 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ On)
229117, 228syl 17 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝑥 → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ On)
230229adantl 469 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝐴 ∧ Lim 𝑥) → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ On)
2313adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴)) → 𝐴 ∈ On)
232 onsseleq 5975 . . . . . . . . . . . . . . . . . . 19 (((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ⊆ 𝐴 ↔ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴 ∨ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴)))
233230, 231, 232syl2an 585 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ⊆ 𝐴 ↔ ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴 ∨ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴)))
234215, 233mpbid 223 . . . . . . . . . . . . . . . . 17 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴 ∨ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴))
235234orcomd 889 . . . . . . . . . . . . . . . 16 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴 ∨ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴))
236235ord 882 . . . . . . . . . . . . . . 15 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (¬ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) = 𝐴 → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴))
237206, 236mpd 15 . . . . . . . . . . . . . 14 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴)
238137ad2antrl 710 . . . . . . . . . . . . . . 15 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴)
239 iscard 9081 . . . . . . . . . . . . . . . 16 ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧𝐴 𝑧𝐴))
240239simprbi 486 . . . . . . . . . . . . . . 15 ((card‘𝐴) = 𝐴 → ∀𝑧𝐴 𝑧𝐴)
241 breq1 4843 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) → (𝑧𝐴 ↔ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ≺ 𝐴))
242241rspccv 3498 . . . . . . . . . . . . . . 15 (∀𝑧𝐴 𝑧𝐴 → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴 → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ≺ 𝐴))
243238, 240, 2423syl 18 . . . . . . . . . . . . . 14 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → ((𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∈ 𝐴 → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ≺ 𝐴))
244237, 243mpd 15 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ≺ 𝐴)
245 domsdomtr 8331 . . . . . . . . . . . . 13 (((𝑅1𝑥) ≼ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ∧ (𝑥 𝑦𝑥 (card‘(𝑅1𝑦))) ≺ 𝐴) → (𝑅1𝑥) ≺ 𝐴)
246107, 244, 245syl2anc 575 . . . . . . . . . . . 12 (((𝑥𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴))) → (𝑅1𝑥) ≺ 𝐴)
247246exp43 425 . . . . . . . . . . 11 (𝑥𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (𝑅1𝑥) ≺ 𝐴))))
248247com4l 92 . . . . . . . . . 10 (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦𝑥 (𝑦𝐴 → (𝑅1𝑦) ≺ 𝐴) → (𝑥𝐴 → (𝑅1𝑥) ≺ 𝐴))))
24913, 17, 21, 28, 61, 248tfinds2 7290 . . . . . . . . 9 (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥𝐴 → (𝑅1𝑥) ≺ 𝐴)))
250249impd 398 . . . . . . . 8 (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥𝐴) → (𝑅1𝑥) ≺ 𝐴))
2519, 250mpcom 38 . . . . . . 7 ((𝐴 ∈ Inacc ∧ 𝑥𝐴) → (𝑅1𝑥) ≺ 𝐴)
252 sdomdom 8217 . . . . . . 7 ((𝑅1𝑥) ≺ 𝐴 → (𝑅1𝑥) ≼ 𝐴)
253251, 252syl 17 . . . . . 6 ((𝐴 ∈ Inacc ∧ 𝑥𝐴) → (𝑅1𝑥) ≼ 𝐴)
254253ralrimiva 3153 . . . . 5 (𝐴 ∈ Inacc → ∀𝑥𝐴 (𝑅1𝑥) ≼ 𝐴)
255 iundom 9646 . . . . 5 ((𝐴 ∈ On ∧ ∀𝑥𝐴 (𝑅1𝑥) ≼ 𝐴) → 𝑥𝐴 (𝑅1𝑥) ≼ (𝐴 × 𝐴))
2563, 254, 255syl2anc 575 . . . 4 (𝐴 ∈ Inacc → 𝑥𝐴 (𝑅1𝑥) ≼ (𝐴 × 𝐴))
2577, 256eqbrtrd 4862 . . 3 (𝐴 ∈ Inacc → (𝑅1𝐴) ≼ (𝐴 × 𝐴))
258 winainf 9798 . . . . 5 (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
2591, 258syl 17 . . . 4 (𝐴 ∈ Inacc → ω ⊆ 𝐴)
260 infxpen 9117 . . . 4 ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
2613, 259, 260syl2anc 575 . . 3 (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴)
262 domentr 8248 . . 3 (((𝑅1𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1𝐴) ≼ 𝐴)
263257, 261, 262syl2anc 575 . 2 (𝐴 ∈ Inacc → (𝑅1𝐴) ≼ 𝐴)
264 fvex 6418 . . 3 (𝑅1𝐴) ∈ V
265122fdmi 6263 . . . . 5 dom 𝑅1 = On
2662, 265syl6eleqr 2895 . . . 4 (𝐴 ∈ Inaccw𝐴 ∈ dom 𝑅1)
267 onssr1 8938 . . . 4 (𝐴 ∈ dom 𝑅1𝐴 ⊆ (𝑅1𝐴))
2681, 266, 2673syl 18 . . 3 (𝐴 ∈ Inacc → 𝐴 ⊆ (𝑅1𝐴))
269 ssdomg 8235 . . 3 ((𝑅1𝐴) ∈ V → (𝐴 ⊆ (𝑅1𝐴) → 𝐴 ≼ (𝑅1𝐴)))
270264, 268, 269mpsyl 68 . 2 (𝐴 ∈ Inacc → 𝐴 ≼ (𝑅1𝐴))
271 sbth 8316 . 2 (((𝑅1𝐴) ≼ 𝐴𝐴 ≼ (𝑅1𝐴)) → (𝑅1𝐴) ≈ 𝐴)
272263, 270, 271syl2anc 575 1 (𝐴 ∈ Inacc → (𝑅1𝐴) ≈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wex 1859  wcel 2158  wne 2977  wral 3095  wrex 3096  Vcvv 3390  cun 3764  wss 3766  c0 4113  ifcif 4276  𝒫 cpw 4348   ciun 4708   class class class wbr 4840  Tr wtr 4942   × cxp 5306  dom cdm 5308  cres 5310  ccom 5312  Ord word 5932  Oncon0 5933  Lim wlim 5934  suc csuc 5935  Fun wfun 6092   Fn wfn 6093  wf 6094  cfv 6098  ωcom 7292  cen 8186  cdom 8187  csdm 8188  𝑅1cr1 8869  cardccrd 9041  cfccf 9043  Inaccwcwina 9786  Inacccina 9787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-ac2 9567
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-er 7976  df-map 8091  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-oi 8651  df-r1 8871  df-rank 8872  df-card 9045  df-cf 9047  df-acn 9048  df-ac 9219  df-wina 9788  df-ina 9789
This theorem is referenced by:  r1omALT  9880  inatsk  9882
  Copyright terms: Public domain W3C validator