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

Theorem fseqenlem1 9236
 Description: Lemma for fseqen 9239. (Contributed by Mario Carneiro, 17-May-2015.)
Hypotheses
Ref Expression
fseqenlem.a (𝜑𝐴𝑉)
fseqenlem.b (𝜑𝐵𝐴)
fseqenlem.f (𝜑𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
fseqenlem.g 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))), {⟨∅, 𝐵⟩})
Assertion
Ref Expression
fseqenlem1 ((𝜑𝐶 ∈ ω) → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴)
Distinct variable groups:   𝑓,𝑛,𝑥,𝐹   𝐴,𝑓,𝑛,𝑥   𝜑,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑥,𝑓,𝑛)   𝐶(𝑥,𝑓,𝑛)   𝐺(𝑥,𝑓,𝑛)   𝑉(𝑥,𝑓,𝑛)

Proof of Theorem fseqenlem1
Dummy variables 𝑦 𝑎 𝑏 𝑧 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6493 . . . . . 6 (𝑦 = 𝐶 → (𝐺𝑦) = (𝐺𝐶))
2 f1eq1 6393 . . . . . 6 ((𝐺𝑦) = (𝐺𝐶) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴))
31, 2syl 17 . . . . 5 (𝑦 = 𝐶 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴))
4 oveq2 6978 . . . . . 6 (𝑦 = 𝐶 → (𝐴𝑚 𝑦) = (𝐴𝑚 𝐶))
5 f1eq2 6394 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 𝐶) → ((𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
64, 5syl 17 . . . . 5 (𝑦 = 𝐶 → ((𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
73, 6bitrd 271 . . . 4 (𝑦 = 𝐶 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
87imbi2d 333 . . 3 (𝑦 = 𝐶 → ((𝜑 → (𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴) ↔ (𝜑 → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴)))
9 fveq2 6493 . . . . . . 7 (𝑦 = ∅ → (𝐺𝑦) = (𝐺‘∅))
10 snex 5182 . . . . . . . 8 {⟨∅, 𝐵⟩} ∈ V
11 fseqenlem.g . . . . . . . . 9 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))), {⟨∅, 𝐵⟩})
1211seqom0g 7888 . . . . . . . 8 ({⟨∅, 𝐵⟩} ∈ V → (𝐺‘∅) = {⟨∅, 𝐵⟩})
1310, 12ax-mp 5 . . . . . . 7 (𝐺‘∅) = {⟨∅, 𝐵⟩}
149, 13syl6eq 2824 . . . . . 6 (𝑦 = ∅ → (𝐺𝑦) = {⟨∅, 𝐵⟩})
15 f1eq1 6393 . . . . . 6 ((𝐺𝑦) = {⟨∅, 𝐵⟩} → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴))
1614, 15syl 17 . . . . 5 (𝑦 = ∅ → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴))
17 oveq2 6978 . . . . . 6 (𝑦 = ∅ → (𝐴𝑚 𝑦) = (𝐴𝑚 ∅))
18 f1eq2 6394 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 ∅) → ({⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
1917, 18syl 17 . . . . 5 (𝑦 = ∅ → ({⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
2016, 19bitrd 271 . . . 4 (𝑦 = ∅ → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
21 fveq2 6493 . . . . . 6 (𝑦 = 𝑚 → (𝐺𝑦) = (𝐺𝑚))
22 f1eq1 6393 . . . . . 6 ((𝐺𝑦) = (𝐺𝑚) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
2321, 22syl 17 . . . . 5 (𝑦 = 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
24 oveq2 6978 . . . . . 6 (𝑦 = 𝑚 → (𝐴𝑚 𝑦) = (𝐴𝑚 𝑚))
25 f1eq2 6394 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 𝑚) → ((𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
2624, 25syl 17 . . . . 5 (𝑦 = 𝑚 → ((𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
2723, 26bitrd 271 . . . 4 (𝑦 = 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
28 fveq2 6493 . . . . . 6 (𝑦 = suc 𝑚 → (𝐺𝑦) = (𝐺‘suc 𝑚))
29 f1eq1 6393 . . . . . 6 ((𝐺𝑦) = (𝐺‘suc 𝑚) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
3028, 29syl 17 . . . . 5 (𝑦 = suc 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
31 oveq2 6978 . . . . . 6 (𝑦 = suc 𝑚 → (𝐴𝑚 𝑦) = (𝐴𝑚 suc 𝑚))
32 f1eq2 6394 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 suc 𝑚) → ((𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
3331, 32syl 17 . . . . 5 (𝑦 = suc 𝑚 → ((𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
3430, 33bitrd 271 . . . 4 (𝑦 = suc 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
35 0ex 5062 . . . . . . . 8 ∅ ∈ V
36 fseqenlem.b . . . . . . . 8 (𝜑𝐵𝐴)
37 f1osng 6478 . . . . . . . 8 ((∅ ∈ V ∧ 𝐵𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
3835, 36, 37sylancr 578 . . . . . . 7 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
39 f1of1 6437 . . . . . . 7 ({⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵} → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
4038, 39syl 17 . . . . . 6 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
4136snssd 4610 . . . . . 6 (𝜑 → {𝐵} ⊆ 𝐴)
42 f1ss 6403 . . . . . 6 (({⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵} ∧ {𝐵} ⊆ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1𝐴)
4340, 41, 42syl2anc 576 . . . . 5 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1𝐴)
44 fseqenlem.a . . . . . . . 8 (𝜑𝐴𝑉)
45 map0e 8237 . . . . . . . 8 (𝐴𝑉 → (𝐴𝑚 ∅) = 1o)
4644, 45syl 17 . . . . . . 7 (𝜑 → (𝐴𝑚 ∅) = 1o)
47 df1o2 7910 . . . . . . 7 1o = {∅}
4846, 47syl6eq 2824 . . . . . 6 (𝜑 → (𝐴𝑚 ∅) = {∅})
49 f1eq2 6394 . . . . . 6 ((𝐴𝑚 ∅) = {∅} → ({⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1𝐴))
5048, 49syl 17 . . . . 5 (𝜑 → ({⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1𝐴))
5143, 50mpbird 249 . . . 4 (𝜑 → {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴)
5211seqomsuc 7889 . . . . . . . . . 10 (𝑚 ∈ ω → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)))
5352ad2antrl 715 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)))
54 vex 3412 . . . . . . . . . 10 𝑚 ∈ V
55 fvex 6506 . . . . . . . . . 10 (𝐺𝑚) ∈ V
56 reseq1 5682 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑥𝑎) = (𝑧𝑎))
5756fveq2d 6497 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑏‘(𝑥𝑎)) = (𝑏‘(𝑧𝑎)))
58 fveq1 6492 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥𝑎) = (𝑧𝑎))
5957, 58oveq12d 6988 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)) = ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)))
6059cbvmptv 5022 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)))
61 suceq 6088 . . . . . . . . . . . . . . 15 (𝑎 = 𝑚 → suc 𝑎 = suc 𝑚)
6261adantr 473 . . . . . . . . . . . . . 14 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → suc 𝑎 = suc 𝑚)
6362oveq2d 6986 . . . . . . . . . . . . 13 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝐴𝑚 suc 𝑎) = (𝐴𝑚 suc 𝑚))
64 simpr 477 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → 𝑏 = (𝐺𝑚))
65 reseq2 5683 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑚 → (𝑧𝑎) = (𝑧𝑚))
6665adantr 473 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧𝑎) = (𝑧𝑚))
6764, 66fveq12d 6500 . . . . . . . . . . . . . 14 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑏‘(𝑧𝑎)) = ((𝐺𝑚)‘(𝑧𝑚)))
68 simpl 475 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → 𝑎 = 𝑚)
6968fveq2d 6497 . . . . . . . . . . . . . 14 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧𝑎) = (𝑧𝑚))
7067, 69oveq12d 6988 . . . . . . . . . . . . 13 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)) = (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
7163, 70mpteq12dv 5006 . . . . . . . . . . . 12 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
7260, 71syl5eq 2820 . . . . . . . . . . 11 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
73 nfcv 2926 . . . . . . . . . . . 12 𝑎(𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))
74 nfcv 2926 . . . . . . . . . . . 12 𝑏(𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))
75 nfcv 2926 . . . . . . . . . . . 12 𝑛(𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
76 nfcv 2926 . . . . . . . . . . . 12 𝑓(𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
77 suceq 6088 . . . . . . . . . . . . . . 15 (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎)
7877adantr 473 . . . . . . . . . . . . . 14 ((𝑛 = 𝑎𝑓 = 𝑏) → suc 𝑛 = suc 𝑎)
7978oveq2d 6986 . . . . . . . . . . . . 13 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝐴𝑚 suc 𝑛) = (𝐴𝑚 suc 𝑎))
80 simpr 477 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → 𝑓 = 𝑏)
81 reseq2 5683 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑎 → (𝑥𝑛) = (𝑥𝑎))
8281adantr 473 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥𝑛) = (𝑥𝑎))
8380, 82fveq12d 6500 . . . . . . . . . . . . . 14 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑓‘(𝑥𝑛)) = (𝑏‘(𝑥𝑎)))
84 simpl 475 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → 𝑛 = 𝑎)
8584fveq2d 6497 . . . . . . . . . . . . . 14 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥𝑛) = (𝑥𝑎))
8683, 85oveq12d 6988 . . . . . . . . . . . . 13 ((𝑛 = 𝑎𝑓 = 𝑏) → ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)) = ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
8779, 86mpteq12dv 5006 . . . . . . . . . . . 12 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))) = (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))))
8873, 74, 75, 76, 87cbvmpo 7058 . . . . . . . . . . 11 (𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))))
89 ovex 7002 . . . . . . . . . . . 12 (𝐴𝑚 suc 𝑚) ∈ V
9089mptex 6806 . . . . . . . . . . 11 (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))) ∈ V
9172, 88, 90ovmpoa 7115 . . . . . . . . . 10 ((𝑚 ∈ V ∧ (𝐺𝑚) ∈ V) → (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
9254, 55, 91mp2an 679 . . . . . . . . 9 (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
9353, 92syl6eq 2824 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
94 fseqenlem.f . . . . . . . . . . 11 (𝜑𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
9594ad2antrr 713 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
96 f1of 6438 . . . . . . . . . 10 (𝐹:(𝐴 × 𝐴)–1-1-onto𝐴𝐹:(𝐴 × 𝐴)⟶𝐴)
9795, 96syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)⟶𝐴)
98 f1f 6398 . . . . . . . . . . . 12 ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
9998ad2antll 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
10099adantr 473 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
101 elmapi 8220 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴𝑚 suc 𝑚) → 𝑧:suc 𝑚𝐴)
102101adantl 474 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝑧:suc 𝑚𝐴)
103 sssucid 6100 . . . . . . . . . . . 12 𝑚 ⊆ suc 𝑚
104 fssres 6367 . . . . . . . . . . . 12 ((𝑧:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑧𝑚):𝑚𝐴)
105102, 103, 104sylancl 577 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚):𝑚𝐴)
10644ad2antrr 713 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐴𝑉)
107 elmapg 8211 . . . . . . . . . . . 12 ((𝐴𝑉𝑚 ∈ V) → ((𝑧𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑧𝑚):𝑚𝐴))
108106, 54, 107sylancl 577 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → ((𝑧𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑧𝑚):𝑚𝐴))
109105, 108mpbird 249 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚) ∈ (𝐴𝑚 𝑚))
110100, 109ffvelrnd 6671 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → ((𝐺𝑚)‘(𝑧𝑚)) ∈ 𝐴)
11154sucid 6102 . . . . . . . . . 10 𝑚 ∈ suc 𝑚
112 ffvelrn 6668 . . . . . . . . . 10 ((𝑧:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑧𝑚) ∈ 𝐴)
113102, 111, 112sylancl 577 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚) ∈ 𝐴)
11497, 110, 113fovrnd 7130 . . . . . . . 8 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) ∈ 𝐴)
11593, 114fmpt3d 6697 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)⟶𝐴)
116 elmapi 8220 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐴𝑚 suc 𝑚) → 𝑎:suc 𝑚𝐴)
117116ad2antrl 715 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑎:suc 𝑚𝐴)
118117ffnd 6339 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑎 Fn suc 𝑚)
119 elmapi 8220 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐴𝑚 suc 𝑚) → 𝑏:suc 𝑚𝐴)
120119ad2antll 716 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑏:suc 𝑚𝐴)
121120ffnd 6339 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑏 Fn suc 𝑚)
122103a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑚 ⊆ suc 𝑚)
123 fvreseq 6629 . . . . . . . . . . . 12 (((𝑎 Fn suc 𝑚𝑏 Fn suc 𝑚) ∧ 𝑚 ⊆ suc 𝑚) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥)))
124118, 121, 122, 123syl21anc 825 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥)))
125 fveq2 6493 . . . . . . . . . . . . . . 15 (𝑥 = 𝑚 → (𝑎𝑥) = (𝑎𝑚))
126 fveq2 6493 . . . . . . . . . . . . . . 15 (𝑥 = 𝑚 → (𝑏𝑥) = (𝑏𝑚))
127125, 126eqeq12d 2787 . . . . . . . . . . . . . 14 (𝑥 = 𝑚 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑚) = (𝑏𝑚)))
12854, 127ralsn 4487 . . . . . . . . . . . . 13 (∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑚) = (𝑏𝑚))
129128bicomi 216 . . . . . . . . . . . 12 ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))
130129a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
131124, 130anbi12d 621 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚)) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))))
13293adantr 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
133132fveq1d 6495 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎))
134 reseq1 5682 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎 → (𝑧𝑚) = (𝑎𝑚))
135134fveq2d 6497 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → ((𝐺𝑚)‘(𝑧𝑚)) = ((𝐺𝑚)‘(𝑎𝑚)))
136 fveq1 6492 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (𝑧𝑚) = (𝑎𝑚))
137135, 136oveq12d 6988 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
138 eqid 2772 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
139 ovex 7002 . . . . . . . . . . . . . . . 16 (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)) ∈ V
140137, 138, 139fvmpt 6589 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝐴𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
141140ad2antrl 715 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
142133, 141eqtrd 2808 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
143 df-ov 6973 . . . . . . . . . . . . 13 (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)) = (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩)
144142, 143syl6eq 2824 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩))
145132fveq1d 6495 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏))
146 reseq1 5682 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑏 → (𝑧𝑚) = (𝑏𝑚))
147146fveq2d 6497 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → ((𝐺𝑚)‘(𝑧𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)))
148 fveq1 6492 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → (𝑧𝑚) = (𝑏𝑚))
149147, 148oveq12d 6988 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑏 → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
150 ovex 7002 . . . . . . . . . . . . . . . 16 (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)) ∈ V
151149, 138, 150fvmpt 6589 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐴𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
152151ad2antll 716 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
153145, 152eqtrd 2808 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
154 df-ov 6973 . . . . . . . . . . . . 13 (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩)
155153, 154syl6eq 2824 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
156144, 155eqeq12d 2787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩)))
15794ad2antrr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
158 f1of1 6437 . . . . . . . . . . . . . 14 (𝐹:(𝐴 × 𝐴)–1-1-onto𝐴𝐹:(𝐴 × 𝐴)–1-1𝐴)
159157, 158syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1𝐴)
16099adantr 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
161 fssres 6367 . . . . . . . . . . . . . . . . 17 ((𝑎:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑎𝑚):𝑚𝐴)
162117, 103, 161sylancl 577 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚):𝑚𝐴)
16344ad2antrr 713 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐴𝑉)
164 elmapg 8211 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝑚 ∈ V) → ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑎𝑚):𝑚𝐴))
165163, 54, 164sylancl 577 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑎𝑚):𝑚𝐴))
166162, 165mpbird 249 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚) ∈ (𝐴𝑚 𝑚))
167160, 166ffvelrnd 6671 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺𝑚)‘(𝑎𝑚)) ∈ 𝐴)
168 ffvelrn 6668 . . . . . . . . . . . . . . 15 ((𝑎:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑎𝑚) ∈ 𝐴)
169117, 111, 168sylancl 577 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚) ∈ 𝐴)
170167, 169opelxpd 5438 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ ∈ (𝐴 × 𝐴))
171 fssres 6367 . . . . . . . . . . . . . . . . 17 ((𝑏:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑏𝑚):𝑚𝐴)
172120, 103, 171sylancl 577 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚):𝑚𝐴)
173 elmapg 8211 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝑚 ∈ V) → ((𝑏𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑏𝑚):𝑚𝐴))
174163, 54, 173sylancl 577 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑏𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑏𝑚):𝑚𝐴))
175172, 174mpbird 249 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚) ∈ (𝐴𝑚 𝑚))
176160, 175ffvelrnd 6671 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺𝑚)‘(𝑏𝑚)) ∈ 𝐴)
177 ffvelrn 6668 . . . . . . . . . . . . . . 15 ((𝑏:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑏𝑚) ∈ 𝐴)
178120, 111, 177sylancl 577 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚) ∈ 𝐴)
179176, 178opelxpd 5438 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ∈ (𝐴 × 𝐴))
180 f1fveq 6839 . . . . . . . . . . . . 13 ((𝐹:(𝐴 × 𝐴)–1-1𝐴 ∧ (⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ ∈ (𝐴 × 𝐴) ∧ ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ∈ (𝐴 × 𝐴))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
181159, 170, 179, 180syl12anc 824 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
182 fvex 6506 . . . . . . . . . . . . 13 ((𝐺𝑚)‘(𝑎𝑚)) ∈ V
183 fvex 6506 . . . . . . . . . . . . 13 (𝑎𝑚) ∈ V
184182, 183opth 5218 . . . . . . . . . . . 12 (⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ↔ (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚)))
185181, 184syl6bb 279 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚))))
186 simplrr 765 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)
187 f1fveq 6839 . . . . . . . . . . . . 13 (((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 ∧ ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ∧ (𝑏𝑚) ∈ (𝐴𝑚 𝑚))) → (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ↔ (𝑎𝑚) = (𝑏𝑚)))
188186, 166, 175, 187syl12anc 824 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ↔ (𝑎𝑚) = (𝑏𝑚)))
189188anbi1d 620 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚)) ↔ ((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚))))
190156, 185, 1893bitrd 297 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ ((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚))))
191 eqfnfv 6621 . . . . . . . . . . . 12 ((𝑎 Fn suc 𝑚𝑏 Fn suc 𝑚) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥)))
192118, 121, 191syl2anc 576 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥)))
193 df-suc 6029 . . . . . . . . . . . . 13 suc 𝑚 = (𝑚 ∪ {𝑚})
194193raleqi 3347 . . . . . . . . . . . 12 (∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎𝑥) = (𝑏𝑥))
195 ralunb 4051 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎𝑥) = (𝑏𝑥) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
196194, 195bitri 267 . . . . . . . . . . 11 (∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
197192, 196syl6bb 279 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))))
198131, 190, 1973bitr4d 303 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ 𝑎 = 𝑏))
199198biimpd 221 . . . . . . . 8 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
200199ralrimivva 3135 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → ∀𝑎 ∈ (𝐴𝑚 suc 𝑚)∀𝑏 ∈ (𝐴𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
201 dff13 6832 . . . . . . 7 ((𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴 ↔ ((𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)⟶𝐴 ∧ ∀𝑎 ∈ (𝐴𝑚 suc 𝑚)∀𝑏 ∈ (𝐴𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)))
202115, 200, 201sylanbrc 575 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴)
203202expr 449 . . . . 5 ((𝜑𝑚 ∈ ω) → ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
204203expcom 406 . . . 4 (𝑚 ∈ ω → (𝜑 → ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴)))
20520, 27, 34, 51, 204finds2 7419 . . 3 (𝑦 ∈ ω → (𝜑 → (𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴))
2068, 205vtoclga 3487 . 2 (𝐶 ∈ ω → (𝜑 → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
207206impcom 399 1 ((𝜑𝐶 ∈ ω) → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2048  ∀wral 3082  Vcvv 3409   ∪ cun 3823   ⊆ wss 3825  ∅c0 4173  {csn 4435  ⟨cop 4441   ↦ cmpt 5002   × cxp 5398   ↾ cres 5402  suc csuc 6025   Fn wfn 6177  ⟶wf 6178  –1-1→wf1 6179  –1-1-onto→wf1o 6181  ‘cfv 6182  (class class class)co 6970   ∈ cmpo 6972  ωcom 7390  seq𝜔cseqom 7879  1oc1o 7890   ↑𝑚 cmap 8198 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-seqom 7880  df-1o 7897  df-map 8200 This theorem is referenced by:  fseqenlem2  9237
 Copyright terms: Public domain W3C validator