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

Theorem axdc2lem 10445
Description: Lemma for axdc2 10446. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹𝑥), and show that the "function" described by ax-dc 10443 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 1955 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
43abbii 2800 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
5 dmopab 5914 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
6 df-rab 3431 . . . . . . . 8 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
74, 5, 63eqtr4i 2768 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
82, 7eqtri 2758 . . . . . 6 dom 𝑅 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
9 ffvelcdm 7082 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10 eldifsni 4792 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
11 n0 4345 . . . . . . . . . 10 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
1210, 11sylib 217 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
139, 12syl 17 . . . . . . . 8 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
1413ralrimiva 3144 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
15 rabid2 3462 . . . . . . 7 (𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} ↔ ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
1614, 15sylibr 233 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
178, 16eqtr4id 2789 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
1817neeq1d 2998 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
1918biimparc 478 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20 eldifi 4125 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝐴)
21 elelpwi 4611 . . . . . . . . . . 11 ((𝑦 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝒫 𝐴) → 𝑦𝐴)
2221expcom 412 . . . . . . . . . 10 ((𝐹𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
239, 20, 223syl 18 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
2423expimpd 452 . . . . . . . 8 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2524exlimdv 1934 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2625alrimiv 1928 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
271rneqi 5935 . . . . . . . . 9 ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
28 rnopab 5952 . . . . . . . . 9 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
2927, 28eqtri 2758 . . . . . . . 8 ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3029sseq1i 4009 . . . . . . 7 (ran 𝑅𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴)
31 abss 4056 . . . . . . 7 ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3230, 31bitri 274 . . . . . 6 (ran 𝑅𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3326, 32sylibr 233 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅𝐴)
3433, 17sseqtrrd 4022 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
3534adantl 480 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36 fvrn0 6920 . . . . . . . . . 10 (𝐹𝑥) ∈ (ran 𝐹 ∪ {∅})
37 elssuni 4940 . . . . . . . . . 10 ((𝐹𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅}))
3836, 37ax-mp 5 . . . . . . . . 9 (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅})
3938sseli 3977 . . . . . . . 8 (𝑦 ∈ (𝐹𝑥) → 𝑦 (ran 𝐹 ∪ {∅}))
4039anim2i 615 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅})))
4140ssopab2i 5549 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
42 df-xp 5681 . . . . . 6 (𝐴 × (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
4341, 1, 423sstr4i 4024 . . . . 5 𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅}))
44 axdc2lem.1 . . . . . 6 𝐴 ∈ V
45 frn 6723 . . . . . . . . . 10 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4645adantl 480 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4744pwex 5377 . . . . . . . . . . 11 𝒫 𝐴 ∈ V
4847difexi 5327 . . . . . . . . . 10 (𝒫 𝐴 ∖ {∅}) ∈ V
4948ssex 5320 . . . . . . . . 9 (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
5046, 49syl 17 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
51 p0ex 5381 . . . . . . . 8 {∅} ∈ V
52 unexg 7738 . . . . . . . 8 ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
5350, 51, 52sylancl 584 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
5453uniexd 7734 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
55 xpexg 7739 . . . . . 6 ((𝐴 ∈ V ∧ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
5644, 54, 55sylancr 585 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
57 ssexg 5322 . . . . 5 ((𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅})) ∧ (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
5843, 56, 57sylancr 585 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
59 n0 4345 . . . . . . . . 9 (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
60 vex 3476 . . . . . . . . . . 11 𝑥 ∈ V
6160eldm 5899 . . . . . . . . . 10 (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
6261exbii 1848 . . . . . . . . 9 (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥𝑦 𝑥𝑟𝑦)
6359, 62bitr2i 275 . . . . . . . 8 (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
64 dmeq 5902 . . . . . . . . 9 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
6564neeq1d 2998 . . . . . . . 8 (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
6663, 65bitrid 282 . . . . . . 7 (𝑟 = 𝑅 → (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
67 rneq 5934 . . . . . . . 8 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
6867, 64sseq12d 4014 . . . . . . 7 (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
6966, 68anbi12d 629 . . . . . 6 (𝑟 = 𝑅 → ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
70 breq 5149 . . . . . . . 8 (𝑟 = 𝑅 → ((𝑘)𝑟(‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
7170ralbidv 3175 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7271exbidv 1922 . . . . . 6 (𝑟 = 𝑅 → (∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7369, 72imbi12d 343 . . . . 5 (𝑟 = 𝑅 → (((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))))
74 ax-dc 10443 . . . . 5 ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘))
7573, 74vtoclg 3541 . . . 4 (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7658, 75syl 17 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7719, 35, 76mp2and 695 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))
78 simpr 483 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
79 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘) = (𝑥))
80 suceq 6429 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
8180fveq2d 6894 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (‘suc 𝑘) = (‘suc 𝑥))
8279, 81breq12d 5160 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑘)𝑅(‘suc 𝑘) ↔ (𝑥)𝑅(‘suc 𝑥)))
8382rspccv 3608 . . . . . . . . . . . . 13 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥)𝑅(‘suc 𝑥)))
84 fvex 6903 . . . . . . . . . . . . . 14 (𝑥) ∈ V
85 fvex 6903 . . . . . . . . . . . . . 14 (‘suc 𝑥) ∈ V
8684, 85breldm 5907 . . . . . . . . . . . . 13 ((𝑥)𝑅(‘suc 𝑥) → (𝑥) ∈ dom 𝑅)
8783, 86syl6 35 . . . . . . . . . . . 12 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥) ∈ dom 𝑅))
8887imp 405 . . . . . . . . . . 11 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
8988adantll 710 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
90 eleq2 2820 . . . . . . . . . . 11 (dom 𝑅 = 𝐴 → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9190ad2antrr 722 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9289, 91mpbid 231 . . . . . . . . 9 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ 𝐴)
93 axdc2lem.3 . . . . . . . . 9 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
9492, 93fmptd 7114 . . . . . . . 8 ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) → 𝐺:ω⟶𝐴)
9594ex 411 . . . . . . 7 (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9617, 95syl 17 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9796impcom 406 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
98 fveq2 6890 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝑥) = (𝑘))
99 fvex 6903 . . . . . . . . . 10 (𝑘) ∈ V
10098, 93, 99fvmpt 6997 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺𝑘) = (𝑘))
101 peano2 7883 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
102 fvex 6903 . . . . . . . . . 10 (‘suc 𝑘) ∈ V
103 fveq2 6890 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑥) = (‘suc 𝑘))
104103, 93fvmptg 6995 . . . . . . . . . 10 ((suc 𝑘 ∈ ω ∧ (‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (‘suc 𝑘))
105101, 102, 104sylancl 584 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (‘suc 𝑘))
106100, 105breq12d 5160 . . . . . . . 8 (𝑘 ∈ ω → ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
107 fvex 6903 . . . . . . . . . 10 (𝐺𝑘) ∈ V
108 fvex 6903 . . . . . . . . . 10 (𝐺‘suc 𝑘) ∈ V
109 eleq1 2819 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑥𝐴 ↔ (𝐺𝑘) ∈ 𝐴))
110 fveq2 6890 . . . . . . . . . . . 12 (𝑥 = (𝐺𝑘) → (𝐹𝑥) = (𝐹‘(𝐺𝑘)))
111110eleq2d 2817 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑦 ∈ (𝐹𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺𝑘))))
112109, 111anbi12d 629 . . . . . . . . . 10 (𝑥 = (𝐺𝑘) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘)))))
113 eleq1 2819 . . . . . . . . . . 11 (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
114113anbi2d 627 . . . . . . . . . 10 (𝑦 = (𝐺‘suc 𝑘) → (((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘))) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
115107, 108, 112, 114, 1brab 5542 . . . . . . . . 9 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
116115simprbi 495 . . . . . . . 8 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
117106, 116syl6bir 253 . . . . . . 7 (𝑘 ∈ ω → ((𝑘)𝑅(‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
118117ralimia 3078 . . . . . 6 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
119118adantr 479 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
120 fvrn0 6920 . . . . . . . . . 10 (𝑥) ∈ (ran ∪ {∅})
121120rgenw 3063 . . . . . . . . 9 𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅})
122 eqid 2730 . . . . . . . . . 10 (𝑥 ∈ ω ↦ (𝑥)) = (𝑥 ∈ ω ↦ (𝑥))
123122fmpt 7110 . . . . . . . . 9 (∀𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}))
124121, 123mpbi 229 . . . . . . . 8 (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅})
125 dcomex 10444 . . . . . . . 8 ω ∈ V
126 vex 3476 . . . . . . . . . 10 ∈ V
127126rnex 7905 . . . . . . . . 9 ran ∈ V
128127, 51unex 7735 . . . . . . . 8 (ran ∪ {∅}) ∈ V
129 fex2 7926 . . . . . . . 8 (((𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}) ∧ ω ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (𝑥)) ∈ V)
130124, 125, 128, 129mp3an 1459 . . . . . . 7 (𝑥 ∈ ω ↦ (𝑥)) ∈ V
13193, 130eqeltri 2827 . . . . . 6 𝐺 ∈ V
132 feq1 6697 . . . . . . 7 (𝑔 = 𝐺 → (𝑔:ω⟶𝐴𝐺:ω⟶𝐴))
133 fveq1 6889 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
134 fveq1 6889 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑘) = (𝐺𝑘))
135134fveq2d 6894 . . . . . . . . 9 (𝑔 = 𝐺 → (𝐹‘(𝑔𝑘)) = (𝐹‘(𝐺𝑘)))
136133, 135eleq12d 2825 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
137136ralbidv 3175 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
138132, 137anbi12d 629 . . . . . 6 (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
139131, 138spcev 3595 . . . . 5 ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
14097, 119, 139syl2anc 582 . . . 4 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
141140ex 411 . . 3 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
142141exlimiv 1931 . 2 (∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
14377, 78, 142sylc 65 1 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1537   = wceq 1539  wex 1779  wcel 2104  {cab 2707  wne 2938  wral 3059  {crab 3430  Vcvv 3472  cdif 3944  cun 3945  wss 3947  c0 4321  𝒫 cpw 4601  {csn 4627   cuni 4907   class class class wbr 5147  {copab 5209  cmpt 5230   × cxp 5673  dom cdm 5675  ran crn 5676  suc csuc 6365  wf 6538  cfv 6542  ωcom 7857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-dc 10443
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-om 7858  df-1o 8468
This theorem is referenced by:  axdc2  10446
  Copyright terms: Public domain W3C validator