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

Theorem axdc2lem 10440
Description: Lemma for axdc2 10441. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹𝑥), and show that the "function" described by ax-dc 10438 can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
axdc2lem.1 𝐴 ∈ V
axdc2lem.2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
axdc2lem.3 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
Assertion
Ref Expression
axdc2lem ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Distinct variable groups:   𝐴,𝑔,   𝑥,𝐴,𝑦,   𝑔,𝐹,   𝑥,𝐹,𝑦   𝑔,𝐺,𝑘   𝑥,𝐺,𝑦,𝑘   𝑅,,𝑘,𝑥
Allowed substitution hints:   𝐴(𝑘)   𝑅(𝑦,𝑔)   𝐹(𝑘)   𝐺()

Proof of Theorem axdc2lem
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 axdc2lem.2 . . . . . . . 8 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
21dmeqi 5903 . . . . . . 7 dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3 19.42v 1958 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
43abbii 2803 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
5 dmopab 5914 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
6 df-rab 3434 . . . . . . . 8 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
74, 5, 63eqtr4i 2771 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
82, 7eqtri 2761 . . . . . 6 dom 𝑅 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
9 ffvelcdm 7081 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10 eldifsni 4793 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
11 n0 4346 . . . . . . . . . 10 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
1210, 11sylib 217 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
139, 12syl 17 . . . . . . . 8 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
1413ralrimiva 3147 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
15 rabid2 3465 . . . . . . 7 (𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} ↔ ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
1614, 15sylibr 233 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
178, 16eqtr4id 2792 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
1817neeq1d 3001 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
1918biimparc 481 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20 eldifi 4126 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝐴)
21 elelpwi 4612 . . . . . . . . . . 11 ((𝑦 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝒫 𝐴) → 𝑦𝐴)
2221expcom 415 . . . . . . . . . 10 ((𝐹𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
239, 20, 223syl 18 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
2423expimpd 455 . . . . . . . 8 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2524exlimdv 1937 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2625alrimiv 1931 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
271rneqi 5935 . . . . . . . . 9 ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
28 rnopab 5952 . . . . . . . . 9 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
2927, 28eqtri 2761 . . . . . . . 8 ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3029sseq1i 4010 . . . . . . 7 (ran 𝑅𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴)
31 abss 4057 . . . . . . 7 ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3230, 31bitri 275 . . . . . 6 (ran 𝑅𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3326, 32sylibr 233 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅𝐴)
3433, 17sseqtrrd 4023 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
3534adantl 483 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36 fvrn0 6919 . . . . . . . . . 10 (𝐹𝑥) ∈ (ran 𝐹 ∪ {∅})
37 elssuni 4941 . . . . . . . . . 10 ((𝐹𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅}))
3836, 37ax-mp 5 . . . . . . . . 9 (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅})
3938sseli 3978 . . . . . . . 8 (𝑦 ∈ (𝐹𝑥) → 𝑦 (ran 𝐹 ∪ {∅}))
4039anim2i 618 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅})))
4140ssopab2i 5550 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
42 df-xp 5682 . . . . . 6 (𝐴 × (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
4341, 1, 423sstr4i 4025 . . . . 5 𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅}))
44 axdc2lem.1 . . . . . 6 𝐴 ∈ V
45 frn 6722 . . . . . . . . . 10 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4645adantl 483 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4744pwex 5378 . . . . . . . . . . 11 𝒫 𝐴 ∈ V
4847difexi 5328 . . . . . . . . . 10 (𝒫 𝐴 ∖ {∅}) ∈ V
4948ssex 5321 . . . . . . . . 9 (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
5046, 49syl 17 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
51 p0ex 5382 . . . . . . . 8 {∅} ∈ V
52 unexg 7733 . . . . . . . 8 ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
5350, 51, 52sylancl 587 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
5453uniexd 7729 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
55 xpexg 7734 . . . . . 6 ((𝐴 ∈ V ∧ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
5644, 54, 55sylancr 588 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
57 ssexg 5323 . . . . 5 ((𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅})) ∧ (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
5843, 56, 57sylancr 588 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
59 n0 4346 . . . . . . . . 9 (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
60 vex 3479 . . . . . . . . . . 11 𝑥 ∈ V
6160eldm 5899 . . . . . . . . . 10 (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
6261exbii 1851 . . . . . . . . 9 (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥𝑦 𝑥𝑟𝑦)
6359, 62bitr2i 276 . . . . . . . 8 (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
64 dmeq 5902 . . . . . . . . 9 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
6564neeq1d 3001 . . . . . . . 8 (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
6663, 65bitrid 283 . . . . . . 7 (𝑟 = 𝑅 → (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
67 rneq 5934 . . . . . . . 8 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
6867, 64sseq12d 4015 . . . . . . 7 (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
6966, 68anbi12d 632 . . . . . 6 (𝑟 = 𝑅 → ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
70 breq 5150 . . . . . . . 8 (𝑟 = 𝑅 → ((𝑘)𝑟(‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
7170ralbidv 3178 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7271exbidv 1925 . . . . . 6 (𝑟 = 𝑅 → (∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7369, 72imbi12d 345 . . . . 5 (𝑟 = 𝑅 → (((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))))
74 ax-dc 10438 . . . . 5 ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘))
7573, 74vtoclg 3557 . . . 4 (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7658, 75syl 17 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7719, 35, 76mp2and 698 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))
78 simpr 486 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
79 fveq2 6889 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘) = (𝑥))
80 suceq 6428 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
8180fveq2d 6893 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (‘suc 𝑘) = (‘suc 𝑥))
8279, 81breq12d 5161 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑘)𝑅(‘suc 𝑘) ↔ (𝑥)𝑅(‘suc 𝑥)))
8382rspccv 3610 . . . . . . . . . . . . 13 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥)𝑅(‘suc 𝑥)))
84 fvex 6902 . . . . . . . . . . . . . 14 (𝑥) ∈ V
85 fvex 6902 . . . . . . . . . . . . . 14 (‘suc 𝑥) ∈ V
8684, 85breldm 5907 . . . . . . . . . . . . 13 ((𝑥)𝑅(‘suc 𝑥) → (𝑥) ∈ dom 𝑅)
8783, 86syl6 35 . . . . . . . . . . . 12 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥) ∈ dom 𝑅))
8887imp 408 . . . . . . . . . . 11 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
8988adantll 713 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
90 eleq2 2823 . . . . . . . . . . 11 (dom 𝑅 = 𝐴 → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9190ad2antrr 725 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9289, 91mpbid 231 . . . . . . . . 9 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ 𝐴)
93 axdc2lem.3 . . . . . . . . 9 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
9492, 93fmptd 7111 . . . . . . . 8 ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) → 𝐺:ω⟶𝐴)
9594ex 414 . . . . . . 7 (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9617, 95syl 17 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9796impcom 409 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
98 fveq2 6889 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝑥) = (𝑘))
99 fvex 6902 . . . . . . . . . 10 (𝑘) ∈ V
10098, 93, 99fvmpt 6996 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺𝑘) = (𝑘))
101 peano2 7878 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
102 fvex 6902 . . . . . . . . . 10 (‘suc 𝑘) ∈ V
103 fveq2 6889 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑥) = (‘suc 𝑘))
104103, 93fvmptg 6994 . . . . . . . . . 10 ((suc 𝑘 ∈ ω ∧ (‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (‘suc 𝑘))
105101, 102, 104sylancl 587 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (‘suc 𝑘))
106100, 105breq12d 5161 . . . . . . . 8 (𝑘 ∈ ω → ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
107 fvex 6902 . . . . . . . . . 10 (𝐺𝑘) ∈ V
108 fvex 6902 . . . . . . . . . 10 (𝐺‘suc 𝑘) ∈ V
109 eleq1 2822 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑥𝐴 ↔ (𝐺𝑘) ∈ 𝐴))
110 fveq2 6889 . . . . . . . . . . . 12 (𝑥 = (𝐺𝑘) → (𝐹𝑥) = (𝐹‘(𝐺𝑘)))
111110eleq2d 2820 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑦 ∈ (𝐹𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺𝑘))))
112109, 111anbi12d 632 . . . . . . . . . 10 (𝑥 = (𝐺𝑘) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘)))))
113 eleq1 2822 . . . . . . . . . . 11 (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
114113anbi2d 630 . . . . . . . . . 10 (𝑦 = (𝐺‘suc 𝑘) → (((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘))) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
115107, 108, 112, 114, 1brab 5543 . . . . . . . . 9 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
116115simprbi 498 . . . . . . . 8 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
117106, 116syl6bir 254 . . . . . . 7 (𝑘 ∈ ω → ((𝑘)𝑅(‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
118117ralimia 3081 . . . . . 6 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
119118adantr 482 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
120 fvrn0 6919 . . . . . . . . . 10 (𝑥) ∈ (ran ∪ {∅})
121120rgenw 3066 . . . . . . . . 9 𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅})
122 eqid 2733 . . . . . . . . . 10 (𝑥 ∈ ω ↦ (𝑥)) = (𝑥 ∈ ω ↦ (𝑥))
123122fmpt 7107 . . . . . . . . 9 (∀𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}))
124121, 123mpbi 229 . . . . . . . 8 (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅})
125 dcomex 10439 . . . . . . . 8 ω ∈ V
126 vex 3479 . . . . . . . . . 10 ∈ V
127126rnex 7900 . . . . . . . . 9 ran ∈ V
128127, 51unex 7730 . . . . . . . 8 (ran ∪ {∅}) ∈ V
129 fex2 7921 . . . . . . . 8 (((𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}) ∧ ω ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (𝑥)) ∈ V)
130124, 125, 128, 129mp3an 1462 . . . . . . 7 (𝑥 ∈ ω ↦ (𝑥)) ∈ V
13193, 130eqeltri 2830 . . . . . 6 𝐺 ∈ V
132 feq1 6696 . . . . . . 7 (𝑔 = 𝐺 → (𝑔:ω⟶𝐴𝐺:ω⟶𝐴))
133 fveq1 6888 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
134 fveq1 6888 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑘) = (𝐺𝑘))
135134fveq2d 6893 . . . . . . . . 9 (𝑔 = 𝐺 → (𝐹‘(𝑔𝑘)) = (𝐹‘(𝐺𝑘)))
136133, 135eleq12d 2828 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
137136ralbidv 3178 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
138132, 137anbi12d 632 . . . . . 6 (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
139131, 138spcev 3597 . . . . 5 ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
14097, 119, 139syl2anc 585 . . . 4 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
141140ex 414 . . 3 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
142141exlimiv 1934 . 2 (∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
14377, 78, 142sylc 65 1 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wne 2941  wral 3062  {crab 3433  Vcvv 3475  cdif 3945  cun 3946  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628   cuni 4908   class class class wbr 5148  {copab 5210  cmpt 5231   × cxp 5674  dom cdm 5676  ran crn 5677  suc csuc 6364  wf 6537  cfv 6541  ωcom 7852
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-dc 10438
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-om 7853  df-1o 8463
This theorem is referenced by:  axdc2  10441
  Copyright terms: Public domain W3C validator