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

Theorem tz9.12lem3 9647
Description: Lemma for tz9.12 9648. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
tz9.12lem.1 𝐴 ∈ V
tz9.12lem.2 𝐹 = (𝑧 ∈ V ↦ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)})
Assertion
Ref Expression
tz9.12lem3 (∀𝑥𝐴𝑦 ∈ On 𝑥 ∈ (𝑅1𝑦) → 𝐴 ∈ (𝑅1‘suc suc (𝐹𝐴)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝐴   𝑥,𝐹,𝑦
Allowed substitution hints:   𝐹(𝑧,𝑣)

Proof of Theorem tz9.12lem3
StepHypRef Expression
1 tz9.12lem.2 . . . . . . . . . . 11 𝐹 = (𝑧 ∈ V ↦ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)})
21funmpt2 6524 . . . . . . . . . 10 Fun 𝐹
3 fveq2 6826 . . . . . . . . . . . . . . 15 (𝑣 = 𝑦 → (𝑅1𝑣) = (𝑅1𝑦))
43eleq2d 2822 . . . . . . . . . . . . . 14 (𝑣 = 𝑦 → (𝑥 ∈ (𝑅1𝑣) ↔ 𝑥 ∈ (𝑅1𝑦)))
54rspcev 3570 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → ∃𝑣 ∈ On 𝑥 ∈ (𝑅1𝑣))
6 rabn0 4333 . . . . . . . . . . . . 13 ({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ On 𝑥 ∈ (𝑅1𝑣))
75, 6sylibr 233 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅)
8 intex 5282 . . . . . . . . . . . 12 ({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅ ↔ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V)
97, 8sylib 217 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V)
10 vex 3445 . . . . . . . . . . . 12 𝑥 ∈ V
11 eleq1w 2819 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑧 ∈ (𝑅1𝑣) ↔ 𝑥 ∈ (𝑅1𝑣)))
1211rabbidv 3411 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
1312inteqd 4900 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
1413eleq1d 2821 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ( {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ V ↔ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V))
151dmmpt 6179 . . . . . . . . . . . . 13 dom 𝐹 = {𝑧 ∈ V ∣ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ V}
1614, 15elrab2 3637 . . . . . . . . . . . 12 (𝑥 ∈ dom 𝐹 ↔ (𝑥 ∈ V ∧ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V))
1710, 16mpbiran 706 . . . . . . . . . . 11 (𝑥 ∈ dom 𝐹 {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V)
189, 17sylibr 233 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → 𝑥 ∈ dom 𝐹)
19 funfvima 7163 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝑥𝐴 → (𝐹𝑥) ∈ (𝐹𝐴)))
202, 18, 19sylancr 587 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → (𝑥𝐴 → (𝐹𝑥) ∈ (𝐹𝐴)))
21 tz9.12lem.1 . . . . . . . . . . 11 𝐴 ∈ V
2221, 1tz9.12lem2 9646 . . . . . . . . . 10 suc (𝐹𝐴) ∈ On
2321, 1tz9.12lem1 9645 . . . . . . . . . . . 12 (𝐹𝐴) ⊆ On
24 onsucuni 7742 . . . . . . . . . . . 12 ((𝐹𝐴) ⊆ On → (𝐹𝐴) ⊆ suc (𝐹𝐴))
2523, 24ax-mp 5 . . . . . . . . . . 11 (𝐹𝐴) ⊆ suc (𝐹𝐴)
2625sseli 3928 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝐹𝐴) → (𝐹𝑥) ∈ suc (𝐹𝐴))
27 r1ord2 9639 . . . . . . . . . 10 (suc (𝐹𝐴) ∈ On → ((𝐹𝑥) ∈ suc (𝐹𝐴) → (𝑅1‘(𝐹𝑥)) ⊆ (𝑅1‘suc (𝐹𝐴))))
2822, 26, 27mpsyl 68 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝐹𝐴) → (𝑅1‘(𝐹𝑥)) ⊆ (𝑅1‘suc (𝐹𝐴)))
2920, 28syl6 35 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → (𝑥𝐴 → (𝑅1‘(𝐹𝑥)) ⊆ (𝑅1‘suc (𝐹𝐴))))
3029imp 407 . . . . . . 7 (((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) ∧ 𝑥𝐴) → (𝑅1‘(𝐹𝑥)) ⊆ (𝑅1‘suc (𝐹𝐴)))
3113, 1fvmptg 6930 . . . . . . . . . . . 12 ((𝑥 ∈ V ∧ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V) → (𝐹𝑥) = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
3210, 31mpan 687 . . . . . . . . . . 11 ( {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ V → (𝐹𝑥) = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
338, 32sylbi 216 . . . . . . . . . 10 ({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅ → (𝐹𝑥) = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
34 ssrab2 4025 . . . . . . . . . . 11 {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ⊆ On
35 onint 7704 . . . . . . . . . . 11 (({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ⊆ On ∧ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅) → {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
3634, 35mpan 687 . . . . . . . . . 10 ({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅ → {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
3733, 36eqeltrd 2837 . . . . . . . . 9 ({𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ≠ ∅ → (𝐹𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)})
38 fveq2 6826 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑥) → (𝑅1𝑦) = (𝑅1‘(𝐹𝑥)))
3938eleq2d 2822 . . . . . . . . . . 11 (𝑦 = (𝐹𝑥) → (𝑥 ∈ (𝑅1𝑦) ↔ 𝑥 ∈ (𝑅1‘(𝐹𝑥))))
404cbvrabv 3413 . . . . . . . . . . 11 {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} = {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1𝑦)}
4139, 40elrab2 3637 . . . . . . . . . 10 ((𝐹𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} ↔ ((𝐹𝑥) ∈ On ∧ 𝑥 ∈ (𝑅1‘(𝐹𝑥))))
4241simprbi 497 . . . . . . . . 9 ((𝐹𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1𝑣)} → 𝑥 ∈ (𝑅1‘(𝐹𝑥)))
437, 37, 423syl 18 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) → 𝑥 ∈ (𝑅1‘(𝐹𝑥)))
4443adantr 481 . . . . . . 7 (((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) ∧ 𝑥𝐴) → 𝑥 ∈ (𝑅1‘(𝐹𝑥)))
4530, 44sseldd 3933 . . . . . 6 (((𝑦 ∈ On ∧ 𝑥 ∈ (𝑅1𝑦)) ∧ 𝑥𝐴) → 𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))
4645exp31 420 . . . . 5 (𝑦 ∈ On → (𝑥 ∈ (𝑅1𝑦) → (𝑥𝐴𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))))
4746com3r 87 . . . 4 (𝑥𝐴 → (𝑦 ∈ On → (𝑥 ∈ (𝑅1𝑦) → 𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))))
4847rexlimdv 3146 . . 3 (𝑥𝐴 → (∃𝑦 ∈ On 𝑥 ∈ (𝑅1𝑦) → 𝑥 ∈ (𝑅1‘suc (𝐹𝐴))))
4948ralimia 3079 . 2 (∀𝑥𝐴𝑦 ∈ On 𝑥 ∈ (𝑅1𝑦) → ∀𝑥𝐴 𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))
50 r1suc 9628 . . . . 5 (suc (𝐹𝐴) ∈ On → (𝑅1‘suc suc (𝐹𝐴)) = 𝒫 (𝑅1‘suc (𝐹𝐴)))
5122, 50ax-mp 5 . . . 4 (𝑅1‘suc suc (𝐹𝐴)) = 𝒫 (𝑅1‘suc (𝐹𝐴))
5251eleq2i 2828 . . 3 (𝐴 ∈ (𝑅1‘suc suc (𝐹𝐴)) ↔ 𝐴 ∈ 𝒫 (𝑅1‘suc (𝐹𝐴)))
5321elpw 4552 . . 3 (𝐴 ∈ 𝒫 (𝑅1‘suc (𝐹𝐴)) ↔ 𝐴 ⊆ (𝑅1‘suc (𝐹𝐴)))
54 dfss3 3920 . . 3 (𝐴 ⊆ (𝑅1‘suc (𝐹𝐴)) ↔ ∀𝑥𝐴 𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))
5552, 53, 543bitri 296 . 2 (𝐴 ∈ (𝑅1‘suc suc (𝐹𝐴)) ↔ ∀𝑥𝐴 𝑥 ∈ (𝑅1‘suc (𝐹𝐴)))
5649, 55sylibr 233 1 (∀𝑥𝐴𝑦 ∈ On 𝑥 ∈ (𝑅1𝑦) → 𝐴 ∈ (𝑅1‘suc suc (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  {crab 3403  Vcvv 3441  wss 3898  c0 4270  𝒫 cpw 4548   cuni 4853   cint 4895  cmpt 5176  dom cdm 5621  cima 5624  Oncon0 6303  suc csuc 6305  Fun wfun 6474  cfv 6480  𝑅1cr1 9620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-ov 7341  df-om 7782  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-r1 9622
This theorem is referenced by:  tz9.12  9648
  Copyright terms: Public domain W3C validator