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

Theorem rankonidlem 8856
Description: Lemma for rankonid 8857. (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 8794 . . . . 5 (Fun 𝑅1 ∧ Lim dom 𝑅1)
21simpri 473 . . . 4 Lim dom 𝑅1
3 limord 5928 . . . 4 (Lim dom 𝑅1 → Ord dom 𝑅1)
42, 3ax-mp 5 . . 3 Ord dom 𝑅1
5 ordelon 5891 . . 3 ((Ord dom 𝑅1𝐴 ∈ dom 𝑅1) → 𝐴 ∈ On)
64, 5mpan 664 . 2 (𝐴 ∈ dom 𝑅1𝐴 ∈ On)
7 eleq1 2838 . . . 4 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑅1𝑦 ∈ dom 𝑅1))
8 eleq1 2838 . . . . 5 (𝑥 = 𝑦 → (𝑥 (𝑅1 “ On) ↔ 𝑦 (𝑅1 “ On)))
9 fveq2 6333 . . . . . 6 (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦))
10 id 22 . . . . . 6 (𝑥 = 𝑦𝑥 = 𝑦)
119, 10eqeq12d 2786 . . . . 5 (𝑥 = 𝑦 → ((rank‘𝑥) = 𝑥 ↔ (rank‘𝑦) = 𝑦))
128, 11anbi12d 610 . . . 4 (𝑥 = 𝑦 → ((𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥) ↔ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
137, 12imbi12d 333 . . 3 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)) ↔ (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦))))
14 eleq1 2838 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝑅1𝐴 ∈ dom 𝑅1))
15 eleq1 2838 . . . . 5 (𝑥 = 𝐴 → (𝑥 (𝑅1 “ On) ↔ 𝐴 (𝑅1 “ On)))
16 fveq2 6333 . . . . . 6 (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴))
17 id 22 . . . . . 6 (𝑥 = 𝐴𝑥 = 𝐴)
1816, 17eqeq12d 2786 . . . . 5 (𝑥 = 𝐴 → ((rank‘𝑥) = 𝑥 ↔ (rank‘𝐴) = 𝐴))
1915, 18anbi12d 610 . . . 4 (𝑥 = 𝐴 → ((𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥) ↔ (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴)))
2014, 19imbi12d 333 . . 3 (𝑥 = 𝐴 → ((𝑥 ∈ dom 𝑅1 → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)) ↔ (𝐴 ∈ dom 𝑅1 → (𝐴 (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))))
21 ordtr1 5911 . . . . . . . . . 10 (Ord dom 𝑅1 → ((𝑦𝑥𝑥 ∈ dom 𝑅1) → 𝑦 ∈ dom 𝑅1))
224, 21ax-mp 5 . . . . . . . . 9 ((𝑦𝑥𝑥 ∈ dom 𝑅1) → 𝑦 ∈ dom 𝑅1)
2322ancoms 455 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1𝑦𝑥) → 𝑦 ∈ dom 𝑅1)
24 pm5.5 350 . . . . . . . 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 3134 . . . . . 6 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 ∈ dom 𝑅1 → (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) ↔ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)))
27 simplr 746 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦𝑥)
28 ordelon 5891 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord dom 𝑅1𝑥 ∈ dom 𝑅1) → 𝑥 ∈ On)
294, 28mpan 664 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ dom 𝑅1𝑥 ∈ On)
3029ad2antrr 699 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ On)
31 eloni 5877 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → Ord 𝑥)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → Ord 𝑥)
33 ordelsuc 7168 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥 ∧ Ord 𝑥) → (𝑦𝑥 ↔ suc 𝑦𝑥))
3427, 32, 33syl2anc 567 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑦𝑥 ↔ suc 𝑦𝑥))
3527, 34mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc 𝑦𝑥)
3623adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ dom 𝑅1)
37 limsuc 7197 . . . . . . . . . . . . . . . . . . . 20 (Lim dom 𝑅1 → (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1))
382, 37ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1)
3936, 38sylib 208 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc 𝑦 ∈ dom 𝑅1)
40 simpll 744 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ dom 𝑅1)
41 r1ord3g 8807 . . . . . . . . . . . . . . . . . 18 ((suc 𝑦 ∈ dom 𝑅1𝑥 ∈ dom 𝑅1) → (suc 𝑦𝑥 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥)))
4239, 40, 41syl2anc 567 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (suc 𝑦𝑥 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥)))
4335, 42mpd 15 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝑥))
44 rankidb 8828 . . . . . . . . . . . . . . . . . 18 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
4544ad2antrl 701 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
46 suceq 5934 . . . . . . . . . . . . . . . . . . 19 ((rank‘𝑦) = 𝑦 → suc (rank‘𝑦) = suc 𝑦)
4746ad2antll 702 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → suc (rank‘𝑦) = suc 𝑦)
4847fveq2d 6337 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc 𝑦))
4945, 48eleqtrd 2852 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1‘suc 𝑦))
5043, 49sseldd 3754 . . . . . . . . . . . . . . 15 (((𝑥 ∈ dom 𝑅1𝑦𝑥) ∧ (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑦 ∈ (𝑅1𝑥))
5150ex 397 . . . . . . . . . . . . . 14 ((𝑥 ∈ dom 𝑅1𝑦𝑥) → ((𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → 𝑦 ∈ (𝑅1𝑥)))
5251ralimdva 3111 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥)))
5352imp 393 . . . . . . . . . . . 12 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥))
54 dfss3 3742 . . . . . . . . . . . 12 (𝑥 ⊆ (𝑅1𝑥) ↔ ∀𝑦𝑥 𝑦 ∈ (𝑅1𝑥))
5553, 54sylibr 224 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ⊆ (𝑅1𝑥))
56 vex 3354 . . . . . . . . . . . 12 𝑥 ∈ V
5756elpw 4304 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 (𝑅1𝑥) ↔ 𝑥 ⊆ (𝑅1𝑥))
5855, 57sylibr 224 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ 𝒫 (𝑅1𝑥))
59 r1sucg 8797 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
6059adantr 466 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
6158, 60eleqtrrd 2853 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ (𝑅1‘suc 𝑥))
62 r1elwf 8824 . . . . . . . . 9 (𝑥 ∈ (𝑅1‘suc 𝑥) → 𝑥 (𝑅1 “ On))
6361, 62syl 17 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 (𝑅1 “ On))
64 rankval3b 8854 . . . . . . . . . 10 (𝑥 (𝑅1 “ On) → (rank‘𝑥) = {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧})
6563, 64syl 17 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (rank‘𝑥) = {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧})
66 eleq1 2838 . . . . . . . . . . . . . . . 16 ((rank‘𝑦) = 𝑦 → ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
6766adantl 467 . . . . . . . . . . . . . . 15 ((𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
6867ralimi 3101 . . . . . . . . . . . . . 14 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → ∀𝑦𝑥 ((rank‘𝑦) ∈ 𝑧𝑦𝑧))
69 ralbi 3216 . . . . . . . . . . . . . 14 (∀𝑦𝑥 ((rank‘𝑦) ∈ 𝑧𝑦𝑧) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦𝑥 𝑦𝑧))
7068, 69syl 17 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦𝑥 𝑦𝑧))
71 dfss3 3742 . . . . . . . . . . . . 13 (𝑥𝑧 ↔ ∀𝑦𝑥 𝑦𝑧)
7270, 71syl6bbr 278 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧𝑥𝑧))
7372rabbidv 3339 . . . . . . . . . . 11 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7473inteqd 4617 . . . . . . . . . 10 (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7574adantl 467 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → {𝑧 ∈ On ∣ ∀𝑦𝑥 (rank‘𝑦) ∈ 𝑧} = {𝑧 ∈ On ∣ 𝑥𝑧})
7629adantr 466 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → 𝑥 ∈ On)
77 intmin 4632 . . . . . . . . . 10 (𝑥 ∈ On → {𝑧 ∈ On ∣ 𝑥𝑧} = 𝑥)
7876, 77syl 17 . . . . . . . . 9 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → {𝑧 ∈ On ∣ 𝑥𝑧} = 𝑥)
7965, 75, 783eqtrd 2809 . . . . . . . 8 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (rank‘𝑥) = 𝑥)
8063, 79jca 497 . . . . . . 7 ((𝑥 ∈ dom 𝑅1 ∧ ∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦)) → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥))
8180ex 397 . . . . . 6 (𝑥 ∈ dom 𝑅1 → (∀𝑦𝑥 (𝑦 (𝑅1 “ On) ∧ (rank‘𝑦) = 𝑦) → (𝑥 (𝑅1 “ On) ∧ (rank‘𝑥) = 𝑥)))
8226, 81sylbid 230 . . . . 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 7205 . 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 196  wa 382   = wceq 1631  wcel 2145  wral 3061  {crab 3065  wss 3724  𝒫 cpw 4298   cuni 4575   cint 4612  dom cdm 5250  cima 5253  Ord word 5866  Oncon0 5867  Lim wlim 5868  suc csuc 5869  Fun wfun 6026  cfv 6032  𝑅1cr1 8790  rankcrnk 8791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-om 7214  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-r1 8792  df-rank 8793
This theorem is referenced by:  rankonid  8857  onwf  8858  onssr1  8859
  Copyright terms: Public domain W3C validator