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

Theorem axdc2lem 9862
 Description: Lemma for axdc2 9863. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 9860 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 5738 . . . . . . 7 dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3 19.42v 1954 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
43abbii 2863 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
5 dmopab 5749 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
6 df-rab 3115 . . . . . . . 8 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
74, 5, 63eqtr4i 2831 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
82, 7eqtri 2821 . . . . . 6 dom 𝑅 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
9 ffvelrn 6827 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10 eldifsni 4683 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
11 n0 4260 . . . . . . . . . 10 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
1210, 11sylib 221 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
139, 12syl 17 . . . . . . . 8 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
1413ralrimiva 3149 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
15 rabid2 3334 . . . . . . 7 (𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} ↔ ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
1614, 15sylibr 237 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
178, 16eqtr4id 2852 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
1817neeq1d 3046 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
1918biimparc 483 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20 eldifi 4054 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝐴)
21 elelpwi 4509 . . . . . . . . . . 11 ((𝑦 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝒫 𝐴) → 𝑦𝐴)
2221expcom 417 . . . . . . . . . 10 ((𝐹𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
239, 20, 223syl 18 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
2423expimpd 457 . . . . . . . 8 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2524exlimdv 1934 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2625alrimiv 1928 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
271rneqi 5772 . . . . . . . . 9 ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
28 rnopab 5791 . . . . . . . . 9 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
2927, 28eqtri 2821 . . . . . . . 8 ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3029sseq1i 3943 . . . . . . 7 (ran 𝑅𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴)
31 abss 3988 . . . . . . 7 ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3230, 31bitri 278 . . . . . 6 (ran 𝑅𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3326, 32sylibr 237 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅𝐴)
3433, 17sseqtrrd 3956 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
3534adantl 485 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36 fvrn0 6674 . . . . . . . . . 10 (𝐹𝑥) ∈ (ran 𝐹 ∪ {∅})
37 elssuni 4831 . . . . . . . . . 10 ((𝐹𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅}))
3836, 37ax-mp 5 . . . . . . . . 9 (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅})
3938sseli 3911 . . . . . . . 8 (𝑦 ∈ (𝐹𝑥) → 𝑦 (ran 𝐹 ∪ {∅}))
4039anim2i 619 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅})))
4140ssopab2i 5403 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
42 df-xp 5526 . . . . . 6 (𝐴 × (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
4341, 1, 423sstr4i 3958 . . . . 5 𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅}))
44 axdc2lem.1 . . . . . 6 𝐴 ∈ V
45 frn 6494 . . . . . . . . . 10 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4645adantl 485 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4744pwex 5247 . . . . . . . . . . 11 𝒫 𝐴 ∈ V
4847difexi 5197 . . . . . . . . . 10 (𝒫 𝐴 ∖ {∅}) ∈ V
4948ssex 5190 . . . . . . . . 9 (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
5046, 49syl 17 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
51 p0ex 5251 . . . . . . . 8 {∅} ∈ V
52 unexg 7455 . . . . . . . 8 ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
5350, 51, 52sylancl 589 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
5453uniexd 7451 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
55 xpexg 7456 . . . . . 6 ((𝐴 ∈ V ∧ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
5644, 54, 55sylancr 590 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
57 ssexg 5192 . . . . 5 ((𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅})) ∧ (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
5843, 56, 57sylancr 590 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
59 n0 4260 . . . . . . . . 9 (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
60 vex 3444 . . . . . . . . . . 11 𝑥 ∈ V
6160eldm 5734 . . . . . . . . . 10 (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
6261exbii 1849 . . . . . . . . 9 (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥𝑦 𝑥𝑟𝑦)
6359, 62bitr2i 279 . . . . . . . 8 (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
64 dmeq 5737 . . . . . . . . 9 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
6564neeq1d 3046 . . . . . . . 8 (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
6663, 65syl5bb 286 . . . . . . 7 (𝑟 = 𝑅 → (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
67 rneq 5771 . . . . . . . 8 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
6867, 64sseq12d 3948 . . . . . . 7 (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
6966, 68anbi12d 633 . . . . . 6 (𝑟 = 𝑅 → ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
70 breq 5033 . . . . . . . 8 (𝑟 = 𝑅 → ((𝑘)𝑟(‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
7170ralbidv 3162 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7271exbidv 1922 . . . . . 6 (𝑟 = 𝑅 → (∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7369, 72imbi12d 348 . . . . 5 (𝑟 = 𝑅 → (((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))))
74 ax-dc 9860 . . . . 5 ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘))
7573, 74vtoclg 3515 . . . 4 (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7658, 75syl 17 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7719, 35, 76mp2and 698 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))
78 simpr 488 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
79 fveq2 6646 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘) = (𝑥))
80 suceq 6225 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
8180fveq2d 6650 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (‘suc 𝑘) = (‘suc 𝑥))
8279, 81breq12d 5044 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑘)𝑅(‘suc 𝑘) ↔ (𝑥)𝑅(‘suc 𝑥)))
8382rspccv 3568 . . . . . . . . . . . . 13 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥)𝑅(‘suc 𝑥)))
84 fvex 6659 . . . . . . . . . . . . . 14 (𝑥) ∈ V
85 fvex 6659 . . . . . . . . . . . . . 14 (‘suc 𝑥) ∈ V
8684, 85breldm 5742 . . . . . . . . . . . . 13 ((𝑥)𝑅(‘suc 𝑥) → (𝑥) ∈ dom 𝑅)
8783, 86syl6 35 . . . . . . . . . . . 12 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥) ∈ dom 𝑅))
8887imp 410 . . . . . . . . . . 11 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
8988adantll 713 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
90 eleq2 2878 . . . . . . . . . . 11 (dom 𝑅 = 𝐴 → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9190ad2antrr 725 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9289, 91mpbid 235 . . . . . . . . 9 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ 𝐴)
93 axdc2lem.3 . . . . . . . . 9 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
9492, 93fmptd 6856 . . . . . . . 8 ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) → 𝐺:ω⟶𝐴)
9594ex 416 . . . . . . 7 (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9617, 95syl 17 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9796impcom 411 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
98 fveq2 6646 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝑥) = (𝑘))
99 fvex 6659 . . . . . . . . . 10 (𝑘) ∈ V
10098, 93, 99fvmpt 6746 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺𝑘) = (𝑘))
101 peano2 7585 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
102 fvex 6659 . . . . . . . . . 10 (‘suc 𝑘) ∈ V
103 fveq2 6646 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑥) = (‘suc 𝑘))
104103, 93fvmptg 6744 . . . . . . . . . 10 ((suc 𝑘 ∈ ω ∧ (‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (‘suc 𝑘))
105101, 102, 104sylancl 589 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (‘suc 𝑘))
106100, 105breq12d 5044 . . . . . . . 8 (𝑘 ∈ ω → ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
107 fvex 6659 . . . . . . . . . 10 (𝐺𝑘) ∈ V
108 fvex 6659 . . . . . . . . . 10 (𝐺‘suc 𝑘) ∈ V
109 eleq1 2877 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑥𝐴 ↔ (𝐺𝑘) ∈ 𝐴))
110 fveq2 6646 . . . . . . . . . . . 12 (𝑥 = (𝐺𝑘) → (𝐹𝑥) = (𝐹‘(𝐺𝑘)))
111110eleq2d 2875 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑦 ∈ (𝐹𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺𝑘))))
112109, 111anbi12d 633 . . . . . . . . . 10 (𝑥 = (𝐺𝑘) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘)))))
113 eleq1 2877 . . . . . . . . . . 11 (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
114113anbi2d 631 . . . . . . . . . 10 (𝑦 = (𝐺‘suc 𝑘) → (((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘))) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
115107, 108, 112, 114, 1brab 5396 . . . . . . . . 9 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
116115simprbi 500 . . . . . . . 8 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
117106, 116syl6bir 257 . . . . . . 7 (𝑘 ∈ ω → ((𝑘)𝑅(‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
118117ralimia 3126 . . . . . 6 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
119118adantr 484 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
120 fvrn0 6674 . . . . . . . . . 10 (𝑥) ∈ (ran ∪ {∅})
121120rgenw 3118 . . . . . . . . 9 𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅})
122 eqid 2798 . . . . . . . . . 10 (𝑥 ∈ ω ↦ (𝑥)) = (𝑥 ∈ ω ↦ (𝑥))
123122fmpt 6852 . . . . . . . . 9 (∀𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}))
124121, 123mpbi 233 . . . . . . . 8 (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅})
125 dcomex 9861 . . . . . . . 8 ω ∈ V
126 vex 3444 . . . . . . . . . 10 ∈ V
127126rnex 7602 . . . . . . . . 9 ran ∈ V
128127, 51unex 7452 . . . . . . . 8 (ran ∪ {∅}) ∈ V
129 fex2 7623 . . . . . . . 8 (((𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}) ∧ ω ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (𝑥)) ∈ V)
130124, 125, 128, 129mp3an 1458 . . . . . . 7 (𝑥 ∈ ω ↦ (𝑥)) ∈ V
13193, 130eqeltri 2886 . . . . . 6 𝐺 ∈ V
132 feq1 6469 . . . . . . 7 (𝑔 = 𝐺 → (𝑔:ω⟶𝐴𝐺:ω⟶𝐴))
133 fveq1 6645 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
134 fveq1 6645 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑘) = (𝐺𝑘))
135134fveq2d 6650 . . . . . . . . 9 (𝑔 = 𝐺 → (𝐹‘(𝑔𝑘)) = (𝐹‘(𝐺𝑘)))
136133, 135eleq12d 2884 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
137136ralbidv 3162 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
138132, 137anbi12d 633 . . . . . 6 (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
139131, 138spcev 3555 . . . . 5 ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
14097, 119, 139syl2anc 587 . . . 4 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
141140ex 416 . . 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 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ∪ cuni 4801   class class class wbr 5031  {copab 5093   ↦ cmpt 5111   × cxp 5518  dom cdm 5520  ran crn 5521  suc csuc 6162  ⟶wf 6321  ‘cfv 6325  ωcom 7563 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-dc 9860 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-fv 6333  df-om 7564  df-1o 8088 This theorem is referenced by:  axdc2  9863
 Copyright terms: Public domain W3C validator