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

Theorem fseqenlem1 8708
Description: Lemma for fseqen 8711. (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 6088 . . . . . 6 (𝑦 = 𝐶 → (𝐺𝑦) = (𝐺𝐶))
2 f1eq1 5994 . . . . . 6 ((𝐺𝑦) = (𝐺𝐶) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴))
31, 2syl 17 . . . . 5 (𝑦 = 𝐶 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴))
4 oveq2 6535 . . . . . 6 (𝑦 = 𝐶 → (𝐴𝑚 𝑦) = (𝐴𝑚 𝐶))
5 f1eq2 5995 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 𝐶) → ((𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
64, 5syl 17 . . . . 5 (𝑦 = 𝐶 → ((𝐺𝐶):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
73, 6bitrd 266 . . . 4 (𝑦 = 𝐶 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
87imbi2d 328 . . 3 (𝑦 = 𝐶 → ((𝜑 → (𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴) ↔ (𝜑 → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴)))
9 fveq2 6088 . . . . . . 7 (𝑦 = ∅ → (𝐺𝑦) = (𝐺‘∅))
10 snex 4830 . . . . . . . 8 {⟨∅, 𝐵⟩} ∈ V
11 fseqenlem.g . . . . . . . . 9 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))), {⟨∅, 𝐵⟩})
1211seqom0g 7416 . . . . . . . 8 ({⟨∅, 𝐵⟩} ∈ V → (𝐺‘∅) = {⟨∅, 𝐵⟩})
1310, 12ax-mp 5 . . . . . . 7 (𝐺‘∅) = {⟨∅, 𝐵⟩}
149, 13syl6eq 2659 . . . . . 6 (𝑦 = ∅ → (𝐺𝑦) = {⟨∅, 𝐵⟩})
15 f1eq1 5994 . . . . . 6 ((𝐺𝑦) = {⟨∅, 𝐵⟩} → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴))
1614, 15syl 17 . . . . 5 (𝑦 = ∅ → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴))
17 oveq2 6535 . . . . . 6 (𝑦 = ∅ → (𝐴𝑚 𝑦) = (𝐴𝑚 ∅))
18 f1eq2 5995 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 ∅) → ({⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
1917, 18syl 17 . . . . 5 (𝑦 = ∅ → ({⟨∅, 𝐵⟩}:(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
2016, 19bitrd 266 . . . 4 (𝑦 = ∅ → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴))
21 fveq2 6088 . . . . . 6 (𝑦 = 𝑚 → (𝐺𝑦) = (𝐺𝑚))
22 f1eq1 5994 . . . . . 6 ((𝐺𝑦) = (𝐺𝑚) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
2321, 22syl 17 . . . . 5 (𝑦 = 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
24 oveq2 6535 . . . . . 6 (𝑦 = 𝑚 → (𝐴𝑚 𝑦) = (𝐴𝑚 𝑚))
25 f1eq2 5995 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 𝑚) → ((𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
2624, 25syl 17 . . . . 5 (𝑦 = 𝑚 → ((𝐺𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
2723, 26bitrd 266 . . . 4 (𝑦 = 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴))
28 fveq2 6088 . . . . . 6 (𝑦 = suc 𝑚 → (𝐺𝑦) = (𝐺‘suc 𝑚))
29 f1eq1 5994 . . . . . 6 ((𝐺𝑦) = (𝐺‘suc 𝑚) → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
3028, 29syl 17 . . . . 5 (𝑦 = suc 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴))
31 oveq2 6535 . . . . . 6 (𝑦 = suc 𝑚 → (𝐴𝑚 𝑦) = (𝐴𝑚 suc 𝑚))
32 f1eq2 5995 . . . . . 6 ((𝐴𝑚 𝑦) = (𝐴𝑚 suc 𝑚) → ((𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
3331, 32syl 17 . . . . 5 (𝑦 = suc 𝑚 → ((𝐺‘suc 𝑚):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
3430, 33bitrd 266 . . . 4 (𝑦 = suc 𝑚 → ((𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴 ↔ (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
35 0ex 4713 . . . . . . . 8 ∅ ∈ V
36 fseqenlem.b . . . . . . . 8 (𝜑𝐵𝐴)
37 f1osng 6074 . . . . . . . 8 ((∅ ∈ V ∧ 𝐵𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
3835, 36, 37sylancr 693 . . . . . . 7 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
39 f1of1 6034 . . . . . . 7 ({⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵} → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
4038, 39syl 17 . . . . . 6 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
4136snssd 4280 . . . . . 6 (𝜑 → {𝐵} ⊆ 𝐴)
42 f1ss 6004 . . . . . 6 (({⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵} ∧ {𝐵} ⊆ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1𝐴)
4340, 41, 42syl2anc 690 . . . . 5 (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1𝐴)
44 fseqenlem.a . . . . . . . 8 (𝜑𝐴𝑉)
45 map0e 7759 . . . . . . . 8 (𝐴𝑉 → (𝐴𝑚 ∅) = 1𝑜)
4644, 45syl 17 . . . . . . 7 (𝜑 → (𝐴𝑚 ∅) = 1𝑜)
47 df1o2 7437 . . . . . . 7 1𝑜 = {∅}
4846, 47syl6eq 2659 . . . . . 6 (𝜑 → (𝐴𝑚 ∅) = {∅})
49 f1eq2 5995 . . . . . 6 ((𝐴𝑚 ∅) = {∅} → ({⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1𝐴))
5048, 49syl 17 . . . . 5 (𝜑 → ({⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1𝐴))
5143, 50mpbird 245 . . . 4 (𝜑 → {⟨∅, 𝐵⟩}:(𝐴𝑚 ∅)–1-1𝐴)
52 fseqenlem.f . . . . . . . . . . . 12 (𝜑𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
5352ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
54 f1of 6035 . . . . . . . . . . 11 (𝐹:(𝐴 × 𝐴)–1-1-onto𝐴𝐹:(𝐴 × 𝐴)⟶𝐴)
5553, 54syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)⟶𝐴)
56 f1f 5999 . . . . . . . . . . . . 13 ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
5756ad2antll 760 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
5857adantr 479 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
59 elmapi 7743 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝐴𝑚 suc 𝑚) → 𝑧:suc 𝑚𝐴)
6059adantl 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝑧:suc 𝑚𝐴)
61 sssucid 5705 . . . . . . . . . . . . 13 𝑚 ⊆ suc 𝑚
62 fssres 5968 . . . . . . . . . . . . 13 ((𝑧:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑧𝑚):𝑚𝐴)
6360, 61, 62sylancl 692 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚):𝑚𝐴)
6444ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → 𝐴𝑉)
65 vex 3175 . . . . . . . . . . . . 13 𝑚 ∈ V
66 elmapg 7735 . . . . . . . . . . . . 13 ((𝐴𝑉𝑚 ∈ V) → ((𝑧𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑧𝑚):𝑚𝐴))
6764, 65, 66sylancl 692 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → ((𝑧𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑧𝑚):𝑚𝐴))
6863, 67mpbird 245 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚) ∈ (𝐴𝑚 𝑚))
6958, 68ffvelrnd 6253 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → ((𝐺𝑚)‘(𝑧𝑚)) ∈ 𝐴)
7065sucid 5707 . . . . . . . . . . 11 𝑚 ∈ suc 𝑚
71 ffvelrn 6250 . . . . . . . . . . 11 ((𝑧:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑧𝑚) ∈ 𝐴)
7260, 70, 71sylancl 692 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (𝑧𝑚) ∈ 𝐴)
7355, 69, 72fovrnd 6682 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ 𝑧 ∈ (𝐴𝑚 suc 𝑚)) → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) ∈ 𝐴)
74 eqid 2609 . . . . . . . . 9 (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
7573, 74fmptd 6277 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))):(𝐴𝑚 suc 𝑚)⟶𝐴)
7611seqomsuc 7417 . . . . . . . . . . 11 (𝑚 ∈ ω → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)))
7776ad2antrl 759 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)))
78 fvex 6098 . . . . . . . . . . 11 (𝐺𝑚) ∈ V
79 reseq1 5298 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑥𝑎) = (𝑧𝑎))
8079fveq2d 6092 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑏‘(𝑥𝑎)) = (𝑏‘(𝑧𝑎)))
81 fveq1 6087 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑥𝑎) = (𝑧𝑎))
8280, 81oveq12d 6545 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)) = ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)))
8382cbvmptv 4672 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)))
84 suceq 5693 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑚 → suc 𝑎 = suc 𝑚)
8584adantr 479 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → suc 𝑎 = suc 𝑚)
8685oveq2d 6543 . . . . . . . . . . . . . 14 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝐴𝑚 suc 𝑎) = (𝐴𝑚 suc 𝑚))
87 simpr 475 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → 𝑏 = (𝐺𝑚))
88 reseq2 5299 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑚 → (𝑧𝑎) = (𝑧𝑚))
8988adantr 479 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧𝑎) = (𝑧𝑚))
9087, 89fveq12d 6094 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑏‘(𝑧𝑎)) = ((𝐺𝑚)‘(𝑧𝑚)))
91 simpl 471 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → 𝑎 = 𝑚)
9291fveq2d 6092 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧𝑎) = (𝑧𝑚))
9390, 92oveq12d 6545 . . . . . . . . . . . . . 14 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎)) = (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
9486, 93mpteq12dv 4657 . . . . . . . . . . . . 13 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑧 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧𝑎))𝐹(𝑧𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
9583, 94syl5eq 2655 . . . . . . . . . . . 12 ((𝑎 = 𝑚𝑏 = (𝐺𝑚)) → (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
96 nfcv 2750 . . . . . . . . . . . . 13 𝑎(𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))
97 nfcv 2750 . . . . . . . . . . . . 13 𝑏(𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))
98 nfcv 2750 . . . . . . . . . . . . 13 𝑛(𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
99 nfcv 2750 . . . . . . . . . . . . 13 𝑓(𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
100 suceq 5693 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎)
101100adantr 479 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → suc 𝑛 = suc 𝑎)
102101oveq2d 6543 . . . . . . . . . . . . . 14 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝐴𝑚 suc 𝑛) = (𝐴𝑚 suc 𝑎))
103 simpr 475 . . . . . . . . . . . . . . . 16 ((𝑛 = 𝑎𝑓 = 𝑏) → 𝑓 = 𝑏)
104 reseq2 5299 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → (𝑥𝑛) = (𝑥𝑎))
105104adantr 479 . . . . . . . . . . . . . . . 16 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥𝑛) = (𝑥𝑎))
106103, 105fveq12d 6094 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑓‘(𝑥𝑛)) = (𝑏‘(𝑥𝑎)))
107 simpl 471 . . . . . . . . . . . . . . . 16 ((𝑛 = 𝑎𝑓 = 𝑏) → 𝑛 = 𝑎)
108107fveq2d 6092 . . . . . . . . . . . . . . 15 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥𝑛) = (𝑥𝑎))
109106, 108oveq12d 6545 . . . . . . . . . . . . . 14 ((𝑛 = 𝑎𝑓 = 𝑏) → ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)) = ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎)))
110102, 109mpteq12dv 4657 . . . . . . . . . . . . 13 ((𝑛 = 𝑎𝑓 = 𝑏) → (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))) = (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))))
11196, 97, 98, 99, 110cbvmpt2 6610 . . . . . . . . . . . 12 (𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛)))) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥𝑎))𝐹(𝑥𝑎))))
112 ovex 6555 . . . . . . . . . . . . 13 (𝐴𝑚 suc 𝑚) ∈ V
113112mptex 6368 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))) ∈ V
11495, 111, 113ovmpt2a 6667 . . . . . . . . . . 11 ((𝑚 ∈ V ∧ (𝐺𝑚) ∈ V) → (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
11565, 78, 114mp2an 703 . . . . . . . . . 10 (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥𝑛))𝐹(𝑥𝑛))))(𝐺𝑚)) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))
11677, 115syl6eq 2659 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
117116feq1d 5929 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → ((𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)⟶𝐴 ↔ (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))):(𝐴𝑚 suc 𝑚)⟶𝐴))
11875, 117mpbird 245 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)⟶𝐴)
119 elmapi 7743 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐴𝑚 suc 𝑚) → 𝑎:suc 𝑚𝐴)
120119ad2antrl 759 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑎:suc 𝑚𝐴)
121 ffn 5944 . . . . . . . . . . . . 13 (𝑎:suc 𝑚𝐴𝑎 Fn suc 𝑚)
122120, 121syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑎 Fn suc 𝑚)
123 elmapi 7743 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝐴𝑚 suc 𝑚) → 𝑏:suc 𝑚𝐴)
124123ad2antll 760 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑏:suc 𝑚𝐴)
125 ffn 5944 . . . . . . . . . . . . 13 (𝑏:suc 𝑚𝐴𝑏 Fn suc 𝑚)
126124, 125syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑏 Fn suc 𝑚)
12761a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝑚 ⊆ suc 𝑚)
128 fvreseq 6212 . . . . . . . . . . . 12 (((𝑎 Fn suc 𝑚𝑏 Fn suc 𝑚) ∧ 𝑚 ⊆ suc 𝑚) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥)))
129122, 126, 127, 128syl21anc 1316 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥)))
130 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑥 = 𝑚 → (𝑎𝑥) = (𝑎𝑚))
131 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑥 = 𝑚 → (𝑏𝑥) = (𝑏𝑚))
132130, 131eqeq12d 2624 . . . . . . . . . . . . . 14 (𝑥 = 𝑚 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑚) = (𝑏𝑚)))
13365, 132ralsn 4168 . . . . . . . . . . . . 13 (∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑚) = (𝑏𝑚))
134133bicomi 212 . . . . . . . . . . . 12 ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))
135134a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) = (𝑏𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
136129, 135anbi12d 742 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚)) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))))
137116adantr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚))))
138137fveq1d 6090 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎))
139 reseq1 5298 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑎 → (𝑧𝑚) = (𝑎𝑚))
140139fveq2d 6092 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → ((𝐺𝑚)‘(𝑧𝑚)) = ((𝐺𝑚)‘(𝑎𝑚)))
141 fveq1 6087 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑎 → (𝑧𝑚) = (𝑎𝑚))
142140, 141oveq12d 6545 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑎 → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
143 ovex 6555 . . . . . . . . . . . . . . . 16 (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)) ∈ V
144142, 74, 143fvmpt 6176 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝐴𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
145144ad2antrl 759 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
146138, 145eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)))
147 df-ov 6530 . . . . . . . . . . . . 13 (((𝐺𝑚)‘(𝑎𝑚))𝐹(𝑎𝑚)) = (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩)
148146, 147syl6eq 2659 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩))
149137fveq1d 6090 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏))
150 reseq1 5298 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑏 → (𝑧𝑚) = (𝑏𝑚))
151150fveq2d 6092 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → ((𝐺𝑚)‘(𝑧𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)))
152 fveq1 6087 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → (𝑧𝑚) = (𝑏𝑚))
153151, 152oveq12d 6545 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑏 → (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
154 ovex 6555 . . . . . . . . . . . . . . . 16 (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)) ∈ V
155153, 74, 154fvmpt 6176 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐴𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
156155ad2antll 760 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴𝑚 suc 𝑚) ↦ (((𝐺𝑚)‘(𝑧𝑚))𝐹(𝑧𝑚)))‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
157149, 156eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)))
158 df-ov 6530 . . . . . . . . . . . . 13 (((𝐺𝑚)‘(𝑏𝑚))𝐹(𝑏𝑚)) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩)
159157, 158syl6eq 2659 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
160148, 159eqeq12d 2624 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ (𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩)))
16152ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1-onto𝐴)
162 f1of1 6034 . . . . . . . . . . . . . 14 (𝐹:(𝐴 × 𝐴)–1-1-onto𝐴𝐹:(𝐴 × 𝐴)–1-1𝐴)
163161, 162syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1𝐴)
16457adantr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺𝑚):(𝐴𝑚 𝑚)⟶𝐴)
165 fssres 5968 . . . . . . . . . . . . . . . . 17 ((𝑎:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑎𝑚):𝑚𝐴)
166120, 61, 165sylancl 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚):𝑚𝐴)
16744ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → 𝐴𝑉)
168 elmapg 7735 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝑚 ∈ V) → ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑎𝑚):𝑚𝐴))
169167, 65, 168sylancl 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑎𝑚):𝑚𝐴))
170166, 169mpbird 245 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚) ∈ (𝐴𝑚 𝑚))
171164, 170ffvelrnd 6253 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺𝑚)‘(𝑎𝑚)) ∈ 𝐴)
172 ffvelrn 6250 . . . . . . . . . . . . . . 15 ((𝑎:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑎𝑚) ∈ 𝐴)
173120, 70, 172sylancl 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎𝑚) ∈ 𝐴)
174 opelxpi 5062 . . . . . . . . . . . . . 14 ((((𝐺𝑚)‘(𝑎𝑚)) ∈ 𝐴 ∧ (𝑎𝑚) ∈ 𝐴) → ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ ∈ (𝐴 × 𝐴))
175171, 173, 174syl2anc 690 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ ∈ (𝐴 × 𝐴))
176 fssres 5968 . . . . . . . . . . . . . . . . 17 ((𝑏:suc 𝑚𝐴𝑚 ⊆ suc 𝑚) → (𝑏𝑚):𝑚𝐴)
177124, 61, 176sylancl 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚):𝑚𝐴)
178 elmapg 7735 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝑚 ∈ V) → ((𝑏𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑏𝑚):𝑚𝐴))
179167, 65, 178sylancl 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝑏𝑚) ∈ (𝐴𝑚 𝑚) ↔ (𝑏𝑚):𝑚𝐴))
180177, 179mpbird 245 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚) ∈ (𝐴𝑚 𝑚))
181164, 180ffvelrnd 6253 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐺𝑚)‘(𝑏𝑚)) ∈ 𝐴)
182 ffvelrn 6250 . . . . . . . . . . . . . . 15 ((𝑏:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑏𝑚) ∈ 𝐴)
183124, 70, 182sylancl 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑏𝑚) ∈ 𝐴)
184 opelxpi 5062 . . . . . . . . . . . . . 14 ((((𝐺𝑚)‘(𝑏𝑚)) ∈ 𝐴 ∧ (𝑏𝑚) ∈ 𝐴) → ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ∈ (𝐴 × 𝐴))
185181, 183, 184syl2anc 690 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ∈ (𝐴 × 𝐴))
186 f1fveq 6398 . . . . . . . . . . . . 13 ((𝐹:(𝐴 × 𝐴)–1-1𝐴 ∧ (⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ ∈ (𝐴 × 𝐴) ∧ ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ∈ (𝐴 × 𝐴))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
187163, 175, 185, 186syl12anc 1315 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ ⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩))
188 fvex 6098 . . . . . . . . . . . . 13 ((𝐺𝑚)‘(𝑎𝑚)) ∈ V
189 fvex 6098 . . . . . . . . . . . . 13 (𝑎𝑚) ∈ V
190188, 189opth 4865 . . . . . . . . . . . 12 (⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩ = ⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩ ↔ (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚)))
191187, 190syl6bb 274 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺𝑚)‘(𝑎𝑚)), (𝑎𝑚)⟩) = (𝐹‘⟨((𝐺𝑚)‘(𝑏𝑚)), (𝑏𝑚)⟩) ↔ (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚))))
192 simplrr 796 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)
193 f1fveq 6398 . . . . . . . . . . . . 13 (((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 ∧ ((𝑎𝑚) ∈ (𝐴𝑚 𝑚) ∧ (𝑏𝑚) ∈ (𝐴𝑚 𝑚))) → (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ↔ (𝑎𝑚) = (𝑏𝑚)))
194192, 170, 180, 193syl12anc 1315 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ↔ (𝑎𝑚) = (𝑏𝑚)))
195194anbi1d 736 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → ((((𝐺𝑚)‘(𝑎𝑚)) = ((𝐺𝑚)‘(𝑏𝑚)) ∧ (𝑎𝑚) = (𝑏𝑚)) ↔ ((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚))))
196160, 191, 1953bitrd 292 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ ((𝑎𝑚) = (𝑏𝑚) ∧ (𝑎𝑚) = (𝑏𝑚))))
197 eqfnfv 6204 . . . . . . . . . . . 12 ((𝑎 Fn suc 𝑚𝑏 Fn suc 𝑚) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥)))
198122, 126, 197syl2anc 690 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥)))
199 df-suc 5632 . . . . . . . . . . . . 13 suc 𝑚 = (𝑚 ∪ {𝑚})
200199raleqi 3118 . . . . . . . . . . . 12 (∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎𝑥) = (𝑏𝑥))
201 ralunb 3755 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎𝑥) = (𝑏𝑥) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
202200, 201bitri 262 . . . . . . . . . . 11 (∀𝑥 ∈ suc 𝑚(𝑎𝑥) = (𝑏𝑥) ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥)))
203198, 202syl6bb 274 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ (∀𝑥𝑚 (𝑎𝑥) = (𝑏𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎𝑥) = (𝑏𝑥))))
204136, 196, 2033bitr4d 298 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ 𝑎 = 𝑏))
205204biimpd 217 . . . . . . . 8 (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) ∧ (𝑎 ∈ (𝐴𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
206205ralrimivva 2953 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → ∀𝑎 ∈ (𝐴𝑚 suc 𝑚)∀𝑏 ∈ (𝐴𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
207 dff13 6394 . . . . . . 7 ((𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴 ↔ ((𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)⟶𝐴 ∧ ∀𝑎 ∈ (𝐴𝑚 suc 𝑚)∀𝑏 ∈ (𝐴𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)))
208118, 206, 207sylanbrc 694 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴)) → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴)
209208expr 640 . . . . 5 ((𝜑𝑚 ∈ ω) → ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴))
210209expcom 449 . . . 4 (𝑚 ∈ ω → (𝜑 → ((𝐺𝑚):(𝐴𝑚 𝑚)–1-1𝐴 → (𝐺‘suc 𝑚):(𝐴𝑚 suc 𝑚)–1-1𝐴)))
21120, 27, 34, 51, 210finds2 6964 . . 3 (𝑦 ∈ ω → (𝜑 → (𝐺𝑦):(𝐴𝑚 𝑦)–1-1𝐴))
2128, 211vtoclga 3244 . 2 (𝐶 ∈ ω → (𝜑 → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴))
213212impcom 444 1 ((𝜑𝐶 ∈ ω) → (𝐺𝐶):(𝐴𝑚 𝐶)–1-1𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  Vcvv 3172  cun 3537  wss 3539  c0 3873  {csn 4124  cop 4130  cmpt 4637   × cxp 5026  cres 5030  suc csuc 5628   Fn wfn 5785  wf 5786  1-1wf1 5787  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cmpt2 6529  ωcom 6935  seq𝜔cseqom 7407  1𝑜c1o 7418  𝑚 cmap 7722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-seqom 7408  df-1o 7425  df-map 7724
This theorem is referenced by:  fseqenlem2  8709
  Copyright terms: Public domain W3C validator