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

Theorem rankonidlem 9586
Description: Lemma for rankonid 9587. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
Assertion
Ref Expression
rankonidlem (𝐴 ∈ dom 𝑅1 → (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))

Proof of Theorem rankonidlem
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r1funlim 9524 . . . . 5 (Fun 𝑅1 ∧ Lim dom 𝑅1)
21simpri 486 . . . 4 Lim dom 𝑅1
3 limord 6325 . . . 4 (Lim dom 𝑅1 → Ord dom 𝑅1)
42, 3ax-mp 5 . . 3 Ord dom 𝑅1
5 ordelon 6290 . . 3 ((Ord dom 𝑅1𝐴 ∈ dom 𝑅1) → 𝐴 ∈ On)
64, 5mpan 687 . 2 (𝐴 ∈ dom 𝑅1𝐴 ∈ On)
7 eleq1 2826 . . . 4 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑅1𝑦 ∈ dom 𝑅1))
8 eleq1 2826 . . . . 5 (𝑥 = 𝑦 → (𝑥 (𝑅1 “ On) ↔ 𝑦 (𝑅1 “ On)))
9 fveq2 6774 . . . . . 6 (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦))
10 id 22 . . . . . 6 (𝑥 = 𝑦𝑥 = 𝑦)
119, 10eqeq12d 2754 . . . . 5 (𝑥 = 𝑦 → ((rank‘𝑥) = 𝑥 ↔ (rank‘𝑦) = 𝑦))
128, 11anbi12d 631 . . . 4 (𝑥 = 𝑦 → ((𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥) ↔ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
137, 12imbi12d 345 . . 3 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)) ↔ (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦))))
14 eleq1 2826 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝑅1𝐴 ∈ dom 𝑅1))
15 eleq1 2826 . . . . 5 (𝑥 = 𝐴 → (𝑥 (𝑅1 “ On) ↔ 𝐴 (𝑅1 “ On)))
16 fveq2 6774 . . . . . 6 (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴))
17 id 22 . . . . . 6 (𝑥 = 𝐴𝑥 = 𝐴)
1816, 17eqeq12d 2754 . . . . 5 (𝑥 = 𝐴 → ((rank‘𝑥) = 𝑥 ↔ (rank‘𝐴) = 𝐴))
1915, 18anbi12d 631 . . . 4 (𝑥 = 𝐴 → ((𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥) ↔ (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴)))
2014, 19imbi12d 345 . . 3 (𝑥 = 𝐴 → ((𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)) ↔ (𝐴 ∈ dom 𝑅1 → (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))))
21 ordtr1 6309 . . . . . . . . . 10 (Ord dom 𝑅1 → ((𝑦𝑥𝑥 ∈ dom 𝑅1) → 𝑦 ∈ dom 𝑅1))
224, 21ax-mp 5 . . . . . . . . 9 ((𝑦𝑥𝑥 ∈ dom 𝑅1) → 𝑦 ∈ dom 𝑅1)
2322ancoms 459 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1𝑦𝑥) → 𝑦 ∈ dom 𝑅1)
24 pm5.5 362 . . . . . . . 8 (𝑦 ∈ dom 𝑅1 → ((𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) ↔ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
2523, 24syl 17 . . . . . . 7 ((𝑥 ∈ dom 𝑅1𝑦𝑥) → ((𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) ↔ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
2625ralbidva 3111 . . . . . 6 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) ↔ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
27 simplr 766 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦𝑥)
28 ordelon 6290 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord dom 𝑅1𝑥 ∈ dom 𝑅1) → 𝑥 ∈ On)
294, 28mpan 687 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ dom 𝑅1𝑥 ∈ On)
3029ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ On)
31 eloni 6276 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → Ord 𝑥)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → Ord 𝑥)
33 ordelsuc 7667 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥 ∧ Ord 𝑥) → (𝑦𝑥 ↔ suc 𝑦𝑥))
3427, 32, 33syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑦𝑥 ↔ suc 𝑦𝑥))
3527, 34mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc 𝑦𝑥)
3623adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ dom 𝑅1)
37 limsuc 7696 . . . . . . . . . . . . . . . . . . . 20 (Lim dom 𝑅1 → (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1))
382, 37ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1)
3936, 38sylib 217 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc 𝑦 ∈ dom 𝑅1)
40 simpll 764 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ dom 𝑅1)
41 r1ord3g 9537 . . . . . . . . . . . . . . . . . 18 ((suc 𝑦 ∈ dom 𝑅1𝑥 ∈ dom 𝑅1) → (suc 𝑦𝑥 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥)))
4239, 40, 41syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (suc 𝑦𝑥 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥)))
4335, 42mpd 15 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥))
44 rankidb 9558 . . . . . . . . . . . . . . . . . 18 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
4544ad2antrl 725 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
46 suceq 6331 . . . . . . . . . . . . . . . . . . 19 ((rank‘𝑦) = 𝑦 → suc (rank‘𝑦) = suc 𝑦)
4746ad2antll 726 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc (rank‘𝑦) = suc 𝑦)
4847fveq2d 6778 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc 𝑦))
4945, 48eleqtrd 2841 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1‘suc 𝑦))
5043, 49sseldd 3922 . . . . . . . . . . . . . . 15 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1𝑥))
5150ex 413 . . . . . . . . . . . . . 14 ((𝑥 ∈ dom 𝑅1𝑦𝑥) → ((𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → 𝑦 ∈ (𝑅1𝑥)))
5251ralimdva 3108 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥)))
5352imp 407 . . . . . . . . . . . 12 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥))
54 dfss3 3909 . . . . . . . . . . . 12 (𝑥 ⊆ (𝑅1𝑥) ↔ ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥))
5553, 54sylibr 233 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ⊆ (𝑅1𝑥))
56 vex 3436 . . . . . . . . . . . 12 𝑥 ∈ V
5756elpw 4537 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 (𝑅1𝑥) ↔ 𝑥 ⊆ (𝑅1𝑥))
5855, 57sylibr 233 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ 𝒫 (𝑅1𝑥))
59 r1sucg 9527 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
6059adantr 481 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
6158, 60eleqtrrd 2842 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ (𝑅1‘suc 𝑥))
62 r1elwf 9554 . . . . . . . . 9 (𝑥 ∈ (𝑅1‘suc 𝑥) → 𝑥 (𝑅1 “ On))
6361, 62syl 17 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 (𝑅1 “ On))
64 rankval3b 9584 . . . . . . . . . 10 (𝑥 (𝑅1 “ On) → (rank‘𝑥) = {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧})
6563, 64syl 17 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (rank‘𝑥) = {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧})
66 eleq1 2826 . . . . . . . . . . . . . . . 16 ((rank‘𝑦) = 𝑦 → ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
6766adantl 482 . . . . . . . . . . . . . . 15 ((𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
6867ralimi 3087 . . . . . . . . . . . . . 14 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ∀𝑦𝑥 ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
69 ralbi 3089 . . . . . . . . . . . . . 14 (∀𝑦𝑥 ((rank‘𝑦) ∈ 𝑧𝑦𝑧) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦𝑥 𝑦𝑧))
7068, 69syl 17 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦𝑥 𝑦𝑧))
71 dfss3 3909 . . . . . . . . . . . . 13 (𝑥𝑧 ↔ ∀𝑦𝑥 𝑦𝑧)
7270, 71bitr4di 289 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧𝑥𝑧))
7372rabbidv 3414 . . . . . . . . . . 11 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7473inteqd 4884 . . . . . . . . . 10 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7574adantl 482 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7629adantr 481 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ On)
77 intmin 4899 . . . . . . . . . 10 (𝑥 ∈ On → {𝑧 ∈ On ∣ 𝑥𝑧} = 𝑥)
7876, 77syl 17 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → {𝑧 ∈ On ∣ 𝑥𝑧} = 𝑥)
7965, 75, 783eqtrd 2782 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (rank‘𝑥) = 𝑥)
8063, 79jca 512 . . . . . . 7 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥))
8180ex 413 . . . . . 6 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)))
8226, 81sylbid 239 . . . . 5 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)))
8382com12 32 . . . 4 (∀𝑦𝑥 (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)))
8483a1i 11 . . 3 (𝑥 ∈ On → (∀𝑦𝑥 (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥))))
8513, 20, 84tfis3 7704 . 2 (𝐴 ∈ On → (𝐴 ∈ dom 𝑅1 → (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴)))
866, 85mpcom 38 1 (𝐴 ∈ dom 𝑅1 → (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wral 3064  {crab 3068  wss 3887  𝒫 cpw 4533   cuni 4839   cint 4879  dom cdm 5589  cima 5592  Ord word 6265  Oncon0 6266  Lim wlim 6267  suc csuc 6268  Fun wfun 6427  cfv 6433  𝑅1cr1 9520  rankcrnk 9521
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-r1 9522  df-rank 9523
This theorem is referenced by:  rankonid  9587  onwf  9588  onssr1  9589
  Copyright terms: Public domain W3C validator