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

Theorem axdc2lem 9308
Description: Lemma for axdc2 9309. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹𝑥), and show that the "function" described by ax-dc 9306 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 6397 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
2 eldifsni 4353 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
3 n0 3964 . . . . . . . . . 10 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
42, 3sylib 208 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
51, 4syl 17 . . . . . . . 8 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → ∃𝑦 𝑦 ∈ (𝐹𝑥))
65ralrimiva 2995 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
7 rabid2 3148 . . . . . . 7 (𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} ↔ ∀𝑥𝐴𝑦 𝑦 ∈ (𝐹𝑥))
86, 7sylibr 224 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
9 axdc2lem.2 . . . . . . . 8 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
109dmeqi 5357 . . . . . . 7 dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
11 19.42v 1921 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
1211abbii 2768 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
13 dmopab 5367 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
14 df-rab 2950 . . . . . . . 8 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
1512, 13, 143eqtr4i 2683 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
1610, 15eqtri 2673 . . . . . 6 dom 𝑅 = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
178, 16syl6reqr 2704 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
1817neeq1d 2882 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
1918biimparc 503 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20 eldifi 3765 . . . . . . . . . 10 ((𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝐴)
21 elelpwi 4204 . . . . . . . . . . 11 ((𝑦 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝒫 𝐴) → 𝑦𝐴)
2221expcom 450 . . . . . . . . . 10 ((𝐹𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
231, 20, 223syl 18 . . . . . . . . 9 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝐴) → (𝑦 ∈ (𝐹𝑥) → 𝑦𝐴))
2423expimpd 628 . . . . . . . 8 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2524exlimdv 1901 . . . . . . 7 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
2625alrimiv 1895 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
279rneqi 5384 . . . . . . . . 9 ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
28 rnopab 5402 . . . . . . . . 9 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
2927, 28eqtri 2673 . . . . . . . 8 ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3029sseq1i 3662 . . . . . . 7 (ran 𝑅𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴)
31 abss 3704 . . . . . . 7 ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3230, 31bitri 264 . . . . . 6 (ran 𝑅𝐴 ↔ ∀𝑦(∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) → 𝑦𝐴))
3326, 32sylibr 224 . . . . 5 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅𝐴)
3433, 17sseqtr4d 3675 . . . 4 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
3534adantl 481 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36 fvrn0 6254 . . . . . . . . . 10 (𝐹𝑥) ∈ (ran 𝐹 ∪ {∅})
37 elssuni 4499 . . . . . . . . . 10 ((𝐹𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅}))
3836, 37ax-mp 5 . . . . . . . . 9 (𝐹𝑥) ⊆ (ran 𝐹 ∪ {∅})
3938sseli 3632 . . . . . . . 8 (𝑦 ∈ (𝐹𝑥) → 𝑦 (ran 𝐹 ∪ {∅}))
4039anim2i 592 . . . . . . 7 ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) → (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅})))
4140ssopab2i 5032 . . . . . 6 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
42 df-xp 5149 . . . . . 6 (𝐴 × (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 (ran 𝐹 ∪ {∅}))}
4341, 9, 423sstr4i 3677 . . . . 5 𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅}))
44 axdc2lem.1 . . . . . 6 𝐴 ∈ V
45 frn 6091 . . . . . . . . . 10 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4645adantl 481 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
4744pwex 4878 . . . . . . . . . . 11 𝒫 𝐴 ∈ V
48 difexg 4841 . . . . . . . . . . 11 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∖ {∅}) ∈ V)
4947, 48ax-mp 5 . . . . . . . . . 10 (𝒫 𝐴 ∖ {∅}) ∈ V
5049ssex 4835 . . . . . . . . 9 (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
5146, 50syl 17 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
52 p0ex 4883 . . . . . . . 8 {∅} ∈ V
53 unexg 7001 . . . . . . . 8 ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
5451, 52, 53sylancl 695 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
55 uniexg 6997 . . . . . . 7 ((ran 𝐹 ∪ {∅}) ∈ V → (ran 𝐹 ∪ {∅}) ∈ V)
5654, 55syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
57 xpexg 7002 . . . . . 6 ((𝐴 ∈ V ∧ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
5844, 56, 57sylancr 696 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V)
59 ssexg 4837 . . . . 5 ((𝑅 ⊆ (𝐴 × (ran 𝐹 ∪ {∅})) ∧ (𝐴 × (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
6043, 58, 59sylancr 696 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
61 n0 3964 . . . . . . . . 9 (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
62 vex 3234 . . . . . . . . . . 11 𝑥 ∈ V
6362eldm 5353 . . . . . . . . . 10 (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
6463exbii 1814 . . . . . . . . 9 (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥𝑦 𝑥𝑟𝑦)
6561, 64bitr2i 265 . . . . . . . 8 (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
66 dmeq 5356 . . . . . . . . 9 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
6766neeq1d 2882 . . . . . . . 8 (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
6865, 67syl5bb 272 . . . . . . 7 (𝑟 = 𝑅 → (∃𝑥𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
69 rneq 5383 . . . . . . . 8 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
7069, 66sseq12d 3667 . . . . . . 7 (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
7168, 70anbi12d 747 . . . . . 6 (𝑟 = 𝑅 → ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
72 breq 4687 . . . . . . . 8 (𝑟 = 𝑅 → ((𝑘)𝑟(‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
7372ralbidv 3015 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7473exbidv 1890 . . . . . 6 (𝑟 = 𝑅 → (∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘) ↔ ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7571, 74imbi12d 333 . . . . 5 (𝑟 = 𝑅 → (((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))))
76 ax-dc 9306 . . . . 5 ((∃𝑥𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃𝑘 ∈ ω (𝑘)𝑟(‘suc 𝑘))
7775, 76vtoclg 3297 . . . 4 (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7860, 77syl 17 . . 3 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)))
7919, 35, 78mp2and 715 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘))
80 simpr 476 . 2 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
81 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘) = (𝑥))
82 suceq 5828 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
8382fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (‘suc 𝑘) = (‘suc 𝑥))
8481, 83breq12d 4698 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑘)𝑅(‘suc 𝑘) ↔ (𝑥)𝑅(‘suc 𝑥)))
8584rspccv 3337 . . . . . . . . . . . . 13 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥)𝑅(‘suc 𝑥)))
86 fvex 6239 . . . . . . . . . . . . . 14 (𝑥) ∈ V
87 fvex 6239 . . . . . . . . . . . . . 14 (‘suc 𝑥) ∈ V
8886, 87breldm 5361 . . . . . . . . . . . . 13 ((𝑥)𝑅(‘suc 𝑥) → (𝑥) ∈ dom 𝑅)
8985, 88syl6 35 . . . . . . . . . . . 12 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝑥 ∈ ω → (𝑥) ∈ dom 𝑅))
9089imp 444 . . . . . . . . . . 11 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
9190adantll 750 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ dom 𝑅)
92 eleq2 2719 . . . . . . . . . . 11 (dom 𝑅 = 𝐴 → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9392ad2antrr 762 . . . . . . . . . 10 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((𝑥) ∈ dom 𝑅 ↔ (𝑥) ∈ 𝐴))
9491, 93mpbid 222 . . . . . . . . 9 (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (𝑥) ∈ 𝐴)
95 axdc2lem.3 . . . . . . . . 9 𝐺 = (𝑥 ∈ ω ↦ (𝑥))
9694, 95fmptd 6425 . . . . . . . 8 ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘)) → 𝐺:ω⟶𝐴)
9796ex 449 . . . . . . 7 (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9817, 97syl 17 . . . . . 6 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → 𝐺:ω⟶𝐴))
9998impcom 445 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
100 fveq2 6229 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝑥) = (𝑘))
101 fvex 6239 . . . . . . . . . 10 (𝑘) ∈ V
102100, 95, 101fvmpt 6321 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺𝑘) = (𝑘))
103 peano2 7128 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
104 fvex 6239 . . . . . . . . . 10 (‘suc 𝑘) ∈ V
105 fveq2 6229 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑥) = (‘suc 𝑘))
106105, 95fvmptg 6319 . . . . . . . . . 10 ((suc 𝑘 ∈ ω ∧ (‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (‘suc 𝑘))
107103, 104, 106sylancl 695 . . . . . . . . 9 (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (‘suc 𝑘))
108102, 107breq12d 4698 . . . . . . . 8 (𝑘 ∈ ω → ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ (𝑘)𝑅(‘suc 𝑘)))
109 fvex 6239 . . . . . . . . . 10 (𝐺𝑘) ∈ V
110 fvex 6239 . . . . . . . . . 10 (𝐺‘suc 𝑘) ∈ V
111 eleq1 2718 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑥𝐴 ↔ (𝐺𝑘) ∈ 𝐴))
112 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = (𝐺𝑘) → (𝐹𝑥) = (𝐹‘(𝐺𝑘)))
113112eleq2d 2716 . . . . . . . . . . 11 (𝑥 = (𝐺𝑘) → (𝑦 ∈ (𝐹𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺𝑘))))
114111, 113anbi12d 747 . . . . . . . . . 10 (𝑥 = (𝐺𝑘) → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘)))))
115 eleq1 2718 . . . . . . . . . . 11 (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
116115anbi2d 740 . . . . . . . . . 10 (𝑦 = (𝐺‘suc 𝑘) → (((𝐺𝑘) ∈ 𝐴𝑦 ∈ (𝐹‘(𝐺𝑘))) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
117109, 110, 114, 116, 9brab 5027 . . . . . . . . 9 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
118117simprbi 479 . . . . . . . 8 ((𝐺𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
119108, 118syl6bir 244 . . . . . . 7 (𝑘 ∈ ω → ((𝑘)𝑅(‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
120119ralimia 2979 . . . . . 6 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
121120adantr 480 . . . . 5 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))
122 fvrn0 6254 . . . . . . . . . 10 (𝑥) ∈ (ran ∪ {∅})
123122rgenw 2953 . . . . . . . . 9 𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅})
124 eqid 2651 . . . . . . . . . 10 (𝑥 ∈ ω ↦ (𝑥)) = (𝑥 ∈ ω ↦ (𝑥))
125124fmpt 6421 . . . . . . . . 9 (∀𝑥 ∈ ω (𝑥) ∈ (ran ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}))
126123, 125mpbi 220 . . . . . . . 8 (𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅})
127 dcomex 9307 . . . . . . . 8 ω ∈ V
128 vex 3234 . . . . . . . . . 10 ∈ V
129128rnex 7142 . . . . . . . . 9 ran ∈ V
130129, 52unex 6998 . . . . . . . 8 (ran ∪ {∅}) ∈ V
131 fex2 7163 . . . . . . . 8 (((𝑥 ∈ ω ↦ (𝑥)):ω⟶(ran ∪ {∅}) ∧ ω ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (𝑥)) ∈ V)
132126, 127, 130, 131mp3an 1464 . . . . . . 7 (𝑥 ∈ ω ↦ (𝑥)) ∈ V
13395, 132eqeltri 2726 . . . . . 6 𝐺 ∈ V
134 feq1 6064 . . . . . . 7 (𝑔 = 𝐺 → (𝑔:ω⟶𝐴𝐺:ω⟶𝐴))
135 fveq1 6228 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
136 fveq1 6228 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑘) = (𝐺𝑘))
137136fveq2d 6233 . . . . . . . . 9 (𝑔 = 𝐺 → (𝐹‘(𝑔𝑘)) = (𝐹‘(𝐺𝑘)))
138135, 137eleq12d 2724 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
139138ralbidv 3015 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))))
140134, 139anbi12d 747 . . . . . 6 (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘)))))
141133, 140spcev 3331 . . . . 5 ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
14299, 121, 141syl2anc 694 . . . 4 ((∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
143142ex 449 . . 3 (∀𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
144143exlimiv 1898 . 2 (∃𝑘 ∈ ω (𝑘)𝑅(‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)))))
14579, 80, 144sylc 65 1 ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wne 2823  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468   class class class wbr 4685  {copab 4745  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  suc csuc 5763  wf 5922  cfv 5926  ωcom 7107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-dc 9306
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-om 7108  df-1o 7605
This theorem is referenced by:  axdc2  9309
  Copyright terms: Public domain W3C validator