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

Theorem axdc4lem 9160
 Description: Lemma for axdc4 9161. (Contributed by Mario Carneiro, 31-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
Hypotheses
Ref Expression
axdc4lem.1 𝐴 ∈ V
axdc4lem.2 𝐺 = (𝑛 ∈ ω, 𝑥𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
Assertion
Ref Expression
axdc4lem ((𝐶𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘))))
Distinct variable groups:   𝑔,𝑘,𝑛,𝑥,𝐴   𝐶,𝑔,𝑘   𝑔,𝐹,𝑛,𝑥   𝑘,𝐺
Allowed substitution hints:   𝐶(𝑥,𝑛)   𝐹(𝑘)   𝐺(𝑥,𝑔,𝑛)

Proof of Theorem axdc4lem
Dummy variables 𝑖 𝑚 𝑠 𝑡 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 6977 . . . 4 ∅ ∈ ω
2 opelxpi 5072 . . . 4 ((∅ ∈ ω ∧ 𝐶𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
31, 2mpan 702 . . 3 (𝐶𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4 simp2 1055 . . . . . . . 8 ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥𝐴) → 𝑛 ∈ ω)
5 fovrn 6702 . . . . . . . 8 ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6 peano2 6978 . . . . . . . . . . 11 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
76snssd 4281 . . . . . . . . . 10 (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8 eldifi 3694 . . . . . . . . . 10 ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9 axdc4lem.1 . . . . . . . . . . . 12 𝐴 ∈ V
109elpw2 4755 . . . . . . . . . . 11 ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11 xpss12 5148 . . . . . . . . . . 11 (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
1210, 11sylan2b 491 . . . . . . . . . 10 (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
137, 8, 12syl2an 493 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14 snex 4835 . . . . . . . . . . 11 {suc 𝑛} ∈ V
15 ovex 6577 . . . . . . . . . . 11 (𝑛𝐹𝑥) ∈ V
1614, 15xpex 6860 . . . . . . . . . 10 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
1716elpw 4114 . . . . . . . . 9 (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
1813, 17sylibr 223 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
194, 5, 18syl2anc 691 . . . . . . 7 ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20 eldifn 3695 . . . . . . . 8 ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
2115elsn 4140 . . . . . . . . . . 11 ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
2221necon3bbii 2829 . . . . . . . . . 10 (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23 vex 3176 . . . . . . . . . . . . 13 𝑛 ∈ V
2423sucex 6903 . . . . . . . . . . . 12 suc 𝑛 ∈ V
2524snnz 4252 . . . . . . . . . . 11 {suc 𝑛} ≠ ∅
26 xpnz 5472 . . . . . . . . . . . 12 (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
2726biimpi 205 . . . . . . . . . . 11 (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
2825, 27mpan 702 . . . . . . . . . 10 ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
2922, 28sylbi 206 . . . . . . . . 9 (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
3016elsn 4140 . . . . . . . . . 10 (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
3130necon3bbii 2829 . . . . . . . . 9 (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
3229, 31sylibr 223 . . . . . . . 8 (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
335, 20, 323syl 18 . . . . . . 7 ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
3419, 33eldifd 3551 . . . . . 6 ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35343expib 1260 . . . . 5 (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
3635ralrimivv 2953 . . . 4 (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37 axdc4lem.2 . . . . 5 𝐺 = (𝑛 ∈ ω, 𝑥𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
3837fmpt2 7126 . . . 4 (∀𝑛 ∈ ω ∀𝑥𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
3936, 38sylib 207 . . 3 (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40 dcomex 9152 . . . . 5 ω ∈ V
4140, 9xpex 6860 . . . 4 (ω × 𝐴) ∈ V
4241axdc3 9159 . . 3 ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃(:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
433, 39, 42syl2an 493 . 2 ((𝐶𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
44 2ndcof 7088 . . . . . . . . 9 (:ω⟶(ω × 𝐴) → (2nd):ω⟶𝐴)
45443ad2ant1 1075 . . . . . . . 8 ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (2nd):ω⟶𝐴)
4645adantl 481 . . . . . . 7 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (2nd):ω⟶𝐴)
47 fex2 7014 . . . . . . . 8 (((2nd):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd) ∈ V)
4840, 9, 47mp3an23 1408 . . . . . . 7 ((2nd):ω⟶𝐴 → (2nd) ∈ V)
4946, 48syl 17 . . . . . 6 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (2nd) ∈ V)
50 fvco3 6185 . . . . . . . . . . 11 ((:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd)‘∅) = (2nd ‘(‘∅)))
511, 50mpan2 703 . . . . . . . . . 10 (:ω⟶(ω × 𝐴) → ((2nd)‘∅) = (2nd ‘(‘∅)))
52513ad2ant1 1075 . . . . . . . . 9 ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((2nd)‘∅) = (2nd ‘(‘∅)))
53 fveq2 6103 . . . . . . . . . 10 ((‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54533ad2ant2 1076 . . . . . . . . 9 ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (2nd ‘(‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
5552, 54eqtrd 2644 . . . . . . . 8 ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((2nd)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56 op2ndg 7072 . . . . . . . . 9 ((∅ ∈ ω ∧ 𝐶𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
571, 56mpan 702 . . . . . . . 8 (𝐶𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
5855, 57sylan9eqr 2666 . . . . . . 7 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((2nd)‘∅) = 𝐶)
59 nfv 1830 . . . . . . . . 9 𝑘 𝐶𝐴
60 nfv 1830 . . . . . . . . . 10 𝑘 :ω⟶(ω × 𝐴)
61 nfv 1830 . . . . . . . . . 10 𝑘(‘∅) = ⟨∅, 𝐶
62 nfra1 2925 . . . . . . . . . 10 𝑘𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))
6360, 61, 62nf3an 1819 . . . . . . . . 9 𝑘(:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
6459, 63nfan 1816 . . . . . . . 8 𝑘(𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
65 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑚 = ∅ → (𝑚) = (‘∅))
66 opeq1 4340 . . . . . . . . . . . . . . . . 17 (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
6765, 66eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑚 = ∅ → ((𝑚) = ⟨𝑚, 𝑧⟩ ↔ (‘∅) = ⟨∅, 𝑧⟩))
6867exbidv 1837 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → (∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(‘∅) = ⟨∅, 𝑧⟩))
69 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑖 → (𝑚) = (𝑖))
70 opeq1 4340 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
7169, 70eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑖 → ((𝑚) = ⟨𝑚, 𝑧⟩ ↔ (𝑖) = ⟨𝑖, 𝑧⟩))
7271exbidv 1837 . . . . . . . . . . . . . . 15 (𝑚 = 𝑖 → (∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩))
73 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑚 = suc 𝑖 → (𝑚) = (‘suc 𝑖))
74 opeq1 4340 . . . . . . . . . . . . . . . . 17 (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
7573, 74eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑚 = suc 𝑖 → ((𝑚) = ⟨𝑚, 𝑧⟩ ↔ (‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
7675exbidv 1837 . . . . . . . . . . . . . . 15 (𝑚 = suc 𝑖 → (∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77 opeq2 4341 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
7877eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((‘∅) = ⟨∅, 𝑧⟩ ↔ (‘∅) = ⟨∅, 𝐶⟩))
7978spcegv 3267 . . . . . . . . . . . . . . . . 17 (𝐶𝐴 → ((‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(‘∅) = ⟨∅, 𝑧⟩))
8079imp 444 . . . . . . . . . . . . . . . 16 ((𝐶𝐴 ∧ (‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(‘∅) = ⟨∅, 𝑧⟩)
81803ad2antr2 1220 . . . . . . . . . . . . . . 15 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ∃𝑧(‘∅) = ⟨∅, 𝑧⟩)
82 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
8482, 83syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(𝑖)) = (𝑖𝐺𝑧))
8584adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(𝑖)) = (𝑖𝐺𝑧))
86 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (𝑖) ∈ (ω × 𝐴))
88 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑖) = ⟨𝑖, 𝑧⟩ → ((𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89 opelxp2 5075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧𝐴)
9088, 89syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑖) = ⟨𝑖, 𝑧⟩ → ((𝑖) ∈ (ω × 𝐴) → 𝑧𝐴))
9187, 90mpan9 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧𝐴)
92 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
9392sneqd 4137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
9593, 94xpeq12d 5064 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
9796xpeq2d 5063 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98 snex 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {suc 𝑖} ∈ V
99 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖𝐹𝑧) ∈ V
10098, 99xpex 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
10195, 97, 37, 100ovmpt2 6694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ω ∧ 𝑧𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
10286, 91, 101syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
10385, 102eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105104fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
106 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑖 → (𝑘) = (𝑖))
107106fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑖 → (𝐺‘(𝑘)) = (𝐺‘(𝑖)))
108105, 107eleq12d 2682 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
109108rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
110109ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
111 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺‘(𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ (‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
112 elxp 5055 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠𝑡((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
113 velsn 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
114 opeq1 4340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115113, 114sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
116115eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 ∈ {suc 𝑖} → ((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
117116biimpac 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118117adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119118eximi 1752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑡((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120119exlimiv 1845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑠𝑡((‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121112, 120sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
122111, 121syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺‘(𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123103, 110, 122sylsyld 59 . . . . . . . . . . . . . . . . . . . . . . 23 (((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
124123expcom 450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖) = ⟨𝑖, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125124exlimiv 1845 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126125com3l 87 . . . . . . . . . . . . . . . . . . . 20 ((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
127 opeq2 4341 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
128127eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → ((‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
129128cbvexv 2263 . . . . . . . . . . . . . . . . . . . 20 (∃𝑡(‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
130126, 129syl8ib 245 . . . . . . . . . . . . . . . . . . 19 ((:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131130impancom 455 . . . . . . . . . . . . . . . . . 18 ((:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑖 ∈ ω → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
1321313adant2 1073 . . . . . . . . . . . . . . . . 17 ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑖 ∈ ω → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133132adantl 481 . . . . . . . . . . . . . . . 16 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑖 ∈ ω → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134133com12 32 . . . . . . . . . . . . . . 15 (𝑖 ∈ ω → ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (∃𝑧(𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
13568, 72, 76, 81, 134finds2 6986 . . . . . . . . . . . . . 14 (𝑚 ∈ ω → ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩))
136135com12 32 . . . . . . . . . . . . 13 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚 ∈ ω → ∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩))
137136ralrimiv 2948 . . . . . . . . . . . 12 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩)
138 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝑚) = (𝑘))
139 opeq1 4340 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
140138, 139eqeq12d 2625 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((𝑚) = ⟨𝑚, 𝑧⟩ ↔ (𝑘) = ⟨𝑘, 𝑧⟩))
141140exbidv 1837 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩))
142141rspccv 3279 . . . . . . . . . . . 12 (∀𝑚 ∈ ω ∃𝑧(𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩))
143137, 142syl 17 . . . . . . . . . . 11 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑘 ∈ ω → ∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩))
1441433impia 1253 . . . . . . . . . 10 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩)
145 simp21 1087 . . . . . . . . . 10 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → :ω⟶(ω × 𝐴))
146 simp3 1056 . . . . . . . . . 10 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
147 rspa 2914 . . . . . . . . . . . 12 ((∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
1481473ad2antl3 1218 . . . . . . . . . . 11 (((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
1491483adant1 1072 . . . . . . . . . 10 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
150 simpl 472 . . . . . . . . . . . . . . . . 17 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘) = ⟨𝑘, 𝑧⟩)
151150fveq2d 6107 . . . . . . . . . . . . . . . 16 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
152 simprr 792 . . . . . . . . . . . . . . . . 17 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
153 ffvelrn 6265 . . . . . . . . . . . . . . . . . . 19 ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (𝑘) ∈ (ω × 𝐴))
154 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 ((𝑘) = ⟨𝑘, 𝑧⟩ → ((𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
155 opelxp2 5075 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧𝐴)
156154, 155syl6bi 242 . . . . . . . . . . . . . . . . . . 19 ((𝑘) = ⟨𝑘, 𝑧⟩ → ((𝑘) ∈ (ω × 𝐴) → 𝑧𝐴))
157153, 156syl5 33 . . . . . . . . . . . . . . . . . 18 ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → 𝑧𝐴))
158157imp 444 . . . . . . . . . . . . . . . . 17 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧𝐴)
159 df-ov 6552 . . . . . . . . . . . . . . . . . 18 (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
160 suceq 5707 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
161160sneqd 4137 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
162 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
163161, 162xpeq12d 5064 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
164 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
165164xpeq2d 5063 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
166 snex 4835 . . . . . . . . . . . . . . . . . . . 20 {suc 𝑘} ∈ V
167 ovex 6577 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐹𝑧) ∈ V
168166, 167xpex 6860 . . . . . . . . . . . . . . . . . . 19 ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
169163, 165, 37, 168ovmpt2 6694 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ω ∧ 𝑧𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170159, 169syl5eqr 2658 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ω ∧ 𝑧𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171152, 158, 170syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
172151, 171eqtrd 2644 . . . . . . . . . . . . . . 15 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
173172eleq2d 2673 . . . . . . . . . . . . . 14 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
174 elxp 5055 . . . . . . . . . . . . . . . . 17 ((‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠𝑡((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
175 peano2 6978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
176 fvco3 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) = (2nd ‘(‘suc 𝑘)))
177175, 176sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) = (2nd ‘(‘suc 𝑘)))
178177adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘suc 𝑘) = (2nd ‘(‘suc 𝑘)))
179 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
180179fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
181178, 180eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
182 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
183 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡 ∈ V
184182, 183op2nd 7068 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
185181, 184syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . 23 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘suc 𝑘) = 𝑡)
186 fvco3 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘𝑘) = (2nd ‘(𝑘)))
187186adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘𝑘) = (2nd ‘(𝑘)))
188 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘) = ⟨𝑘, 𝑧⟩)
189188fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
190187, 189eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
191 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 ∈ V
192 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧 ∈ V
193191, 192op2nd 7068 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
194190, 193syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘𝑘) = 𝑧)
195194oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd)‘𝑘)) = (𝑘𝐹𝑧))
196185, 195eleq12d 2682 . . . . . . . . . . . . . . . . . . . . . 22 ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
197196biimprcd 239 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (𝑘𝐹𝑧) → ((((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑘) = ⟨𝑘, 𝑧⟩) ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
198197exp4c 634 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (𝑘𝐹𝑧) → ((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))))
199198adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))))
200199impcom 445 . . . . . . . . . . . . . . . . . 18 (((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
201200exlimivv 1847 . . . . . . . . . . . . . . . . 17 (∃𝑠𝑡((‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
202174, 201sylbi 206 . . . . . . . . . . . . . . . 16 ((‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
203202com3l 87 . . . . . . . . . . . . . . 15 ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
204203imp 444 . . . . . . . . . . . . . 14 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
205173, 204sylbid 229 . . . . . . . . . . . . 13 (((𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
206205ex 449 . . . . . . . . . . . 12 ((𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
207206exlimiv 1845 . . . . . . . . . . 11 (∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩ → ((:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
2082073imp 1249 . . . . . . . . . 10 ((∃𝑧(𝑘) = ⟨𝑘, 𝑧⟩ ∧ (:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))
209144, 145, 146, 149, 208syl121anc 1323 . . . . . . . . 9 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))
2102093expia 1259 . . . . . . . 8 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑘 ∈ ω → ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
21164, 210ralrimi 2940 . . . . . . 7 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ∀𝑘 ∈ ω ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))
21246, 58, 2113jca 1235 . . . . . 6 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((2nd):ω⟶𝐴 ∧ ((2nd)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
213 feq1 5939 . . . . . . . 8 (𝑔 = (2nd) → (𝑔:ω⟶𝐴 ↔ (2nd):ω⟶𝐴))
214 fveq1 6102 . . . . . . . . 9 (𝑔 = (2nd) → (𝑔‘∅) = ((2nd)‘∅))
215214eqeq1d 2612 . . . . . . . 8 (𝑔 = (2nd) → ((𝑔‘∅) = 𝐶 ↔ ((2nd)‘∅) = 𝐶))
216 fveq1 6102 . . . . . . . . . 10 (𝑔 = (2nd) → (𝑔‘suc 𝑘) = ((2nd)‘suc 𝑘))
217 fveq1 6102 . . . . . . . . . . 11 (𝑔 = (2nd) → (𝑔𝑘) = ((2nd)‘𝑘))
218217oveq2d 6565 . . . . . . . . . 10 (𝑔 = (2nd) → (𝑘𝐹(𝑔𝑘)) = (𝑘𝐹((2nd)‘𝑘)))
219216, 218eleq12d 2682 . . . . . . . . 9 (𝑔 = (2nd) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)) ↔ ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
220219ralbidv 2969 . . . . . . . 8 (𝑔 = (2nd) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)) ↔ ∀𝑘 ∈ ω ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))))
221213, 215, 2203anbi123d 1391 . . . . . . 7 (𝑔 = (2nd) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘))) ↔ ((2nd):ω⟶𝐴 ∧ ((2nd)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘)))))
222221spcegv 3267 . . . . . 6 ((2nd) ∈ V → (((2nd):ω⟶𝐴 ∧ ((2nd)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd)‘suc 𝑘) ∈ (𝑘𝐹((2nd)‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)))))
22349, 212, 222sylc 63 . . . . 5 ((𝐶𝐴 ∧ (:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘))))
224223ex 449 . . . 4 (𝐶𝐴 → ((:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)))))
225224exlimdv 1848 . . 3 (𝐶𝐴 → (∃(:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)))))
226225adantr 480 . 2 ((𝐶𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃(:ω⟶(ω × 𝐴) ∧ (‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘)))))
22743, 226mpd 15 1 ((𝐶𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔𝑘))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131   × cxp 5036   ∘ ccom 5042  suc csuc 5642  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957  2nd c2nd 7058 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-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  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-iun 4457  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-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-1o 7447 This theorem is referenced by:  axdc4  9161
 Copyright terms: Public domain W3C validator