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

Theorem axdc2lem 9153
 Description: Lemma for axdc2 9154. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 9151 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 ffvelrn 6265 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
2 eldifsni 4261 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
3 n0 3890 . . . . . . . . . 10 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
42, 3sylib 207 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
51, 4syl 17 . . . . . . . 8 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
65ralrimiva 2949 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
7 rabid2 3096 . . . . . . 7 (𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} ↔ ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
86, 7sylibr 223 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
9 axdc2lem.2 . . . . . . . 8 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
109dmeqi 5247 . . . . . . 7 dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
11 19.42v 1905 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
1211abbii 2726 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
13 dmopab 5257 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
14 df-rab 2905 . . . . . . . 8 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
1512, 13, 143eqtr4i 2642 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
1610, 15eqtri 2632 . . . . . 6 dom 𝑅 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
178, 16syl6reqr 2663 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
1817neeq1d 2841 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
1918biimparc 503 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20 eldifi 3694 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝐴)
21 elelpwi 4119 . . . . . . . . . . 11 ((𝑦 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝒫 𝐴) → 𝑦𝐴)
2221expcom 450 . . . . . . . . . 10 ((𝐹𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
231, 20, 223syl 18 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
2423expimpd 627 . . . . . . . 8 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2524exlimdv 1848 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2625alrimiv 1842 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
279rneqi 5273 . . . . . . . . 9 ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
28 rnopab 5291 . . . . . . . . 9 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
2927, 28eqtri 2632 . . . . . . . 8 ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3029sseq1i 3592 . . . . . . 7 (ran 𝑅𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴)
31 abss 3634 . . . . . . 7 ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3230, 31bitri 263 . . . . . 6 (ran 𝑅𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3326, 32sylibr 223 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅𝐴)
3433, 17sseqtr4d 3605 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
3534adantl 481 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36 fvrn0 6126 . . . . . . . . . 10 (𝐹𝑥) ∈ (ran 𝐹 ∪ {∅})
37 elssuni 4403 . . . . . . . . . 10 ((𝐹𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅}))
3836, 37ax-mp 5 . . . . . . . . 9 (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅})
3938sseli 3564 . . . . . . . 8 (𝑦 ∈ (𝐹𝑥) → 𝑦 (ran 𝐹 ∪ {∅}))
4039anim2i 591 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅})))
4140ssopab2i 4928 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
42 df-xp 5044 . . . . . 6 (𝐴 × (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
4341, 9, 423sstr4i 3607 . . . . 5 𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅}))
44 axdc2lem.1 . . . . . 6 𝐴 ∈ V
45 frn 5966 . . . . . . . . . 10 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4645adantl 481 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4744pwex 4774 . . . . . . . . . . 11 𝒫 𝐴 ∈ V
48 difexg 4735 . . . . . . . . . . 11 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∖ {∅}) ∈ V)
4947, 48ax-mp 5 . . . . . . . . . 10 (𝒫 𝐴 ∖ {∅}) ∈ V
5049ssex 4730 . . . . . . . . 9 (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
5146, 50syl 17 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
52 p0ex 4779 . . . . . . . 8 {∅} ∈ V
53 unexg 6857 . . . . . . . 8 ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
5451, 52, 53sylancl 693 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
55 uniexg 6853 . . . . . . 7 ((ran 𝐹 ∪ {∅}) ∈ V → (ran 𝐹 ∪ {∅}) ∈ V)
5654, 55syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
57 xpexg 6858 . . . . . 6 ((𝐴 ∈ V ∧ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
5844, 56, 57sylancr 694 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
59 ssexg 4732 . . . . 5 ((𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅})) ∧ (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
6043, 58, 59sylancr 694 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
61 n0 3890 . . . . . . . . 9 (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
62 vex 3176 . . . . . . . . . . 11 𝑥 ∈ V
6362eldm 5243 . . . . . . . . . 10 (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
6463exbii 1764 . . . . . . . . 9 (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥𝑦 𝑥𝑟𝑦)
6561, 64bitr2i 264 . . . . . . . 8 (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
66 dmeq 5246 . . . . . . . . 9 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
6766neeq1d 2841 . . . . . . . 8 (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
6865, 67syl5bb 271 . . . . . . 7 (𝑟 = 𝑅 → (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
69 rneq 5272 . . . . . . . 8 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
7069, 66sseq12d 3597 . . . . . . 7 (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
7168, 70anbi12d 743 . . . . . 6 (𝑟 = 𝑅 → ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
72 breq 4585 . . . . . . . 8 (𝑟 = 𝑅 → ((𝑘)𝑟(‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
7372ralbidv 2969 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7473exbidv 1837 . . . . . 6 (𝑟 = 𝑅 → (∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7571, 74imbi12d 333 . . . . 5 (𝑟 = 𝑅 → (((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))))
76 ax-dc 9151 . . . . 5 ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘))
7775, 76vtoclg 3239 . . . 4 (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7860, 77syl 17 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7919, 35, 78mp2and 711 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))
80 simpr 476 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
81 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘) = (𝑥))
82 suceq 5707 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
8382fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (‘suc 𝑘) = (‘suc 𝑥))
8481, 83breq12d 4596 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑘)𝑅(‘suc 𝑘) ↔ (𝑥)𝑅(‘suc 𝑥)))
8584rspccv 3279 . . . . . . . . . . . . 13 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥)𝑅(‘suc 𝑥)))
86 fvex 6113 . . . . . . . . . . . . . 14 (𝑥) ∈ V
87 fvex 6113 . . . . . . . . . . . . . 14 (‘suc 𝑥) ∈ V
8886, 87breldm 5251 . . . . . . . . . . . . 13 ((𝑥)𝑅(‘suc 𝑥) → (𝑥) ∈ dom 𝑅)
8985, 88syl6 34 . . . . . . . . . . . 12 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥) ∈ dom 𝑅))
9089imp 444 . . . . . . . . . . 11 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
9190adantll 746 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
92 eleq2 2677 . . . . . . . . . . 11 (dom 𝑅 = 𝐴 → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9392ad2antrr 758 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9491, 93mpbid 221 . . . . . . . . 9 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ 𝐴)
95 axdc2lem.3 . . . . . . . . 9 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
9694, 95fmptd 6292 . . . . . . . 8 ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) → 𝐺:ω⟶𝐴)
9796ex 449 . . . . . . 7 (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9817, 97syl 17 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9998impcom 445 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
100 fveq2 6103 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝑥) = (𝑘))
101 fvex 6113 . . . . . . . . . 10 (𝑘) ∈ V
102100, 95, 101fvmpt 6191 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺𝑘) = (𝑘))
103 peano2 6978 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
104 fvex 6113 . . . . . . . . . 10 (‘suc 𝑘) ∈ V
105 fveq2 6103 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑥) = (‘suc 𝑘))
106105, 95fvmptg 6189 . . . . . . . . . 10 ((suc 𝑘 ∈ ω ∧ (‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (‘suc 𝑘))
107103, 104, 106sylancl 693 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (‘suc 𝑘))
108102, 107breq12d 4596 . . . . . . . 8 (𝑘 ∈ ω → ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
109 fvex 6113 . . . . . . . . . 10 (𝐺𝑘) ∈ V
110 fvex 6113 . . . . . . . . . 10 (𝐺‘suc 𝑘) ∈ V
111 eleq1 2676 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑥𝐴 ↔ (𝐺𝑘) ∈ 𝐴))
112 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = (𝐺𝑘) → (𝐹𝑥) = (𝐹‘(𝐺𝑘)))
113112eleq2d 2673 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑦 ∈ (𝐹𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺𝑘))))
114111, 113anbi12d 743 . . . . . . . . . 10 (𝑥 = (𝐺𝑘) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘)))))
115 eleq1 2676 . . . . . . . . . . 11 (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
116115anbi2d 736 . . . . . . . . . 10 (𝑦 = (𝐺‘suc 𝑘) → (((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘))) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
117109, 110, 114, 116, 9brab 4923 . . . . . . . . 9 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
118117simprbi 479 . . . . . . . 8 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
119108, 118syl6bir 243 . . . . . . 7 (𝑘 ∈ ω → ((𝑘)𝑅(‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
120119ralimia 2934 . . . . . 6 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
121120adantr 480 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
122 fvrn0 6126 . . . . . . . . . 10 (𝑥) ∈ (ran ∪ {∅})
123122rgenw 2908 . . . . . . . . 9 𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅})
124 eqid 2610 . . . . . . . . . 10 (𝑥 ∈ ω ↦ (𝑥)) = (𝑥 ∈ ω ↦ (𝑥))
125124fmpt 6289 . . . . . . . . 9 (∀𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}))
126123, 125mpbi 219 . . . . . . . 8 (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅})
127 dcomex 9152 . . . . . . . 8 ω ∈ V
128 vex 3176 . . . . . . . . . 10 ∈ V
129128rnex 6992 . . . . . . . . 9 ran ∈ V
130129, 52unex 6854 . . . . . . . 8 (ran ∪ {∅}) ∈ V
131 fex2 7014 . . . . . . . 8 (((𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}) ∧ ω ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (𝑥)) ∈ V)
132126, 127, 130, 131mp3an 1416 . . . . . . 7 (𝑥 ∈ ω ↦ (𝑥)) ∈ V
13395, 132eqeltri 2684 . . . . . 6 𝐺 ∈ V
134 feq1 5939 . . . . . . 7 (𝑔 = 𝐺 → (𝑔:ω⟶𝐴𝐺:ω⟶𝐴))
135 fveq1 6102 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
136 fveq1 6102 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑘) = (𝐺𝑘))
137136fveq2d 6107 . . . . . . . . 9 (𝑔 = 𝐺 → (𝐹‘(𝑔𝑘)) = (𝐹‘(𝐺𝑘)))
138135, 137eleq12d 2682 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
139138ralbidv 2969 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
140134, 139anbi12d 743 . . . . . 6 (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
141133, 140spcev 3273 . . . . 5 ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
14299, 121, 141syl2anc 691 . . . 4 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
143142ex 449 . . 3 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
144143exlimiv 1845 . 2 (∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
14579, 80, 144sylc 63 1 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   class class class wbr 4583  {copab 4642   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  suc csuc 5642  ⟶wf 5800  ‘cfv 5804  ωcom 6957 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-dc 9151 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-om 6958  df-1o 7447 This theorem is referenced by:  axdc2  9154
 Copyright terms: Public domain W3C validator