Step | Hyp | Ref
| Expression |
1 | | fveq2 6768 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶)) |
2 | | f1eq1 6661 |
. . . . . 6
⊢ ((𝐺‘𝑦) = (𝐺‘𝐶) → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
4 | | oveq2 7276 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝐴 ↑m 𝑦) = (𝐴 ↑m 𝐶)) |
5 | | f1eq2 6662 |
. . . . . 6
⊢ ((𝐴 ↑m 𝑦) = (𝐴 ↑m 𝐶) → ((𝐺‘𝐶):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝐶 → ((𝐺‘𝐶):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)) |
7 | 3, 6 | bitrd 278 |
. . . 4
⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)) |
8 | 7 | imbi2d 340 |
. . 3
⊢ (𝑦 = 𝐶 → ((𝜑 → (𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴) ↔ (𝜑 → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴))) |
9 | | fveq2 6768 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝐺‘𝑦) = (𝐺‘∅)) |
10 | | snex 5357 |
. . . . . . . 8
⊢
{〈∅, 𝐵〉} ∈ V |
11 | | fseqenlem.g |
. . . . . . . . 9
⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) |
12 | 11 | seqom0g 8271 |
. . . . . . . 8
⊢
({〈∅, 𝐵〉} ∈ V → (𝐺‘∅) = {〈∅, 𝐵〉}) |
13 | 10, 12 | ax-mp 5 |
. . . . . . 7
⊢ (𝐺‘∅) =
{〈∅, 𝐵〉} |
14 | 9, 13 | eqtrdi 2795 |
. . . . . 6
⊢ (𝑦 = ∅ → (𝐺‘𝑦) = {〈∅, 𝐵〉}) |
15 | | f1eq1 6661 |
. . . . . 6
⊢ ((𝐺‘𝑦) = {〈∅, 𝐵〉} → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:(𝐴 ↑m 𝑦)–1-1→𝐴)) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:(𝐴 ↑m 𝑦)–1-1→𝐴)) |
17 | | oveq2 7276 |
. . . . . 6
⊢ (𝑦 = ∅ → (𝐴 ↑m 𝑦) = (𝐴 ↑m
∅)) |
18 | | f1eq2 6662 |
. . . . . 6
⊢ ((𝐴 ↑m 𝑦) = (𝐴 ↑m ∅) →
({〈∅, 𝐵〉}:(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝑦 = ∅ →
({〈∅, 𝐵〉}:(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴)) |
20 | 16, 19 | bitrd 278 |
. . . 4
⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴)) |
21 | | fveq2 6768 |
. . . . . 6
⊢ (𝑦 = 𝑚 → (𝐺‘𝑦) = (𝐺‘𝑚)) |
22 | | f1eq1 6661 |
. . . . . 6
⊢ ((𝐺‘𝑦) = (𝐺‘𝑚) → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
24 | | oveq2 7276 |
. . . . . 6
⊢ (𝑦 = 𝑚 → (𝐴 ↑m 𝑦) = (𝐴 ↑m 𝑚)) |
25 | | f1eq2 6662 |
. . . . . 6
⊢ ((𝐴 ↑m 𝑦) = (𝐴 ↑m 𝑚) → ((𝐺‘𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝑚 → ((𝐺‘𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) |
27 | 23, 26 | bitrd 278 |
. . . 4
⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) |
28 | | fveq2 6768 |
. . . . . 6
⊢ (𝑦 = suc 𝑚 → (𝐺‘𝑦) = (𝐺‘suc 𝑚)) |
29 | | f1eq1 6661 |
. . . . . 6
⊢ ((𝐺‘𝑦) = (𝐺‘suc 𝑚) → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
31 | | oveq2 7276 |
. . . . . 6
⊢ (𝑦 = suc 𝑚 → (𝐴 ↑m 𝑦) = (𝐴 ↑m suc 𝑚)) |
32 | | f1eq2 6662 |
. . . . . 6
⊢ ((𝐴 ↑m 𝑦) = (𝐴 ↑m suc 𝑚) → ((𝐺‘suc 𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴)) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝑦 = suc 𝑚 → ((𝐺‘suc 𝑚):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴)) |
34 | 30, 33 | bitrd 278 |
. . . 4
⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴)) |
35 | | 0ex 5234 |
. . . . . . . 8
⊢ ∅
∈ V |
36 | | fseqenlem.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
37 | | f1osng 6752 |
. . . . . . . 8
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝐴) → {〈∅,
𝐵〉}:{∅}–1-1-onto→{𝐵}) |
38 | 35, 36, 37 | sylancr 586 |
. . . . . . 7
⊢ (𝜑 → {〈∅, 𝐵〉}:{∅}–1-1-onto→{𝐵}) |
39 | | f1of1 6711 |
. . . . . . 7
⊢
({〈∅, 𝐵〉}:{∅}–1-1-onto→{𝐵} → {〈∅, 𝐵〉}:{∅}–1-1→{𝐵}) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝜑 → {〈∅, 𝐵〉}:{∅}–1-1→{𝐵}) |
41 | 36 | snssd 4747 |
. . . . . 6
⊢ (𝜑 → {𝐵} ⊆ 𝐴) |
42 | | f1ss 6672 |
. . . . . 6
⊢
(({〈∅, 𝐵〉}:{∅}–1-1→{𝐵} ∧ {𝐵} ⊆ 𝐴) → {〈∅, 𝐵〉}:{∅}–1-1→𝐴) |
43 | 40, 41, 42 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → {〈∅, 𝐵〉}:{∅}–1-1→𝐴) |
44 | | fseqenlem.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
45 | | map0e 8644 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m ∅) =
1o) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑m ∅) =
1o) |
47 | | df1o2 8293 |
. . . . . . 7
⊢
1o = {∅} |
48 | 46, 47 | eqtrdi 2795 |
. . . . . 6
⊢ (𝜑 → (𝐴 ↑m ∅) =
{∅}) |
49 | | f1eq2 6662 |
. . . . . 6
⊢ ((𝐴 ↑m ∅) =
{∅} → ({〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:{∅}–1-1→𝐴)) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → ({〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴 ↔ {〈∅, 𝐵〉}:{∅}–1-1→𝐴)) |
51 | 43, 50 | mpbird 256 |
. . . 4
⊢ (𝜑 → {〈∅, 𝐵〉}:(𝐴 ↑m ∅)–1-1→𝐴) |
52 | 11 | seqomsuc 8272 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚))) |
53 | 52 | ad2antrl 724 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚))) |
54 | | vex 3434 |
. . . . . . . . . 10
⊢ 𝑚 ∈ V |
55 | | fvex 6781 |
. . . . . . . . . 10
⊢ (𝐺‘𝑚) ∈ V |
56 | | reseq1 5882 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑥 ↾ 𝑎) = (𝑧 ↾ 𝑎)) |
57 | 56 | fveq2d 6772 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑏‘(𝑥 ↾ 𝑎)) = (𝑏‘(𝑧 ↾ 𝑎))) |
58 | | fveq1 6767 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥‘𝑎) = (𝑧‘𝑎)) |
59 | 57, 58 | oveq12d 7286 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)) = ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎))) |
60 | 59 | cbvmptv 5191 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎))) |
61 | | suceq 6328 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑚 → suc 𝑎 = suc 𝑚) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → suc 𝑎 = suc 𝑚) |
63 | 62 | oveq2d 7284 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝐴 ↑m suc 𝑎) = (𝐴 ↑m suc 𝑚)) |
64 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑏 = (𝐺‘𝑚)) |
65 | | reseq2 5883 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑚 → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚)) |
67 | 64, 66 | fveq12d 6775 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑏‘(𝑧 ↾ 𝑎)) = ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))) |
68 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑎 = 𝑚) |
69 | 68 | fveq2d 6772 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧‘𝑎) = (𝑧‘𝑚)) |
70 | 67, 69 | oveq12d 7286 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)) = (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) |
71 | 63, 70 | mpteq12dv 5169 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎))) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))) |
72 | 60, 71 | eqtrid 2791 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))) |
73 | | nfcv 2908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))) |
74 | | nfcv 2908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏(𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))) |
75 | | nfcv 2908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) |
76 | | nfcv 2908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓(𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) |
77 | | suceq 6328 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → suc 𝑛 = suc 𝑎) |
79 | 78 | oveq2d 7284 |
. . . . . . . . . . . . 13
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝐴 ↑m suc 𝑛) = (𝐴 ↑m suc 𝑎)) |
80 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑓 = 𝑏) |
81 | | reseq2 5883 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑎 → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎)) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎)) |
83 | 80, 82 | fveq12d 6775 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑓‘(𝑥 ↾ 𝑛)) = (𝑏‘(𝑥 ↾ 𝑎))) |
84 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑛 = 𝑎) |
85 | 84 | fveq2d 6772 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥‘𝑛) = (𝑥‘𝑎)) |
86 | 83, 85 | oveq12d 7286 |
. . . . . . . . . . . . 13
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)) = ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) |
87 | 79, 86 | mpteq12dv 5169 |
. . . . . . . . . . . 12
⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))) = (𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))) |
88 | 73, 74, 75, 76, 87 | cbvmpo 7360 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))) |
89 | | ovex 7301 |
. . . . . . . . . . . 12
⊢ (𝐴 ↑m suc 𝑚) ∈ V |
90 | 89 | mptex 7093 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) ∈ V |
91 | 72, 88, 90 | ovmpoa 7419 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ V ∧ (𝐺‘𝑚) ∈ V) → (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))) |
92 | 54, 55, 91 | mp2an 688 |
. . . . . . . . 9
⊢ (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) |
93 | 53, 92 | eqtrdi 2795 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))) |
94 | | fseqenlem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) |
95 | 94 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) |
96 | | f1of 6712 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)⟶𝐴) |
97 | 95, 96 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → 𝐹:(𝐴 × 𝐴)⟶𝐴) |
98 | | f1f 6666 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴 → (𝐺‘𝑚):(𝐴 ↑m 𝑚)⟶𝐴) |
99 | 98 | ad2antll 725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → (𝐺‘𝑚):(𝐴 ↑m 𝑚)⟶𝐴) |
100 | 99 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → (𝐺‘𝑚):(𝐴 ↑m 𝑚)⟶𝐴) |
101 | | elmapi 8611 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝐴 ↑m suc 𝑚) → 𝑧:suc 𝑚⟶𝐴) |
102 | 101 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → 𝑧:suc 𝑚⟶𝐴) |
103 | | sssucid 6340 |
. . . . . . . . . . . 12
⊢ 𝑚 ⊆ suc 𝑚 |
104 | | fssres 6636 |
. . . . . . . . . . . 12
⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑧 ↾ 𝑚):𝑚⟶𝐴) |
105 | 102, 103,
104 | sylancl 585 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → (𝑧 ↾ 𝑚):𝑚⟶𝐴) |
106 | 44 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → 𝐴 ∈ 𝑉) |
107 | | elmapg 8602 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴)) |
108 | 106, 54, 107 | sylancl 585 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴)) |
109 | 105, 108 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → (𝑧 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚)) |
110 | 100, 109 | ffvelrnd 6956 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) ∈ 𝐴) |
111 | 54 | sucid 6342 |
. . . . . . . . . 10
⊢ 𝑚 ∈ suc 𝑚 |
112 | | ffvelrn 6953 |
. . . . . . . . . 10
⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑧‘𝑚) ∈ 𝐴) |
113 | 102, 111,
112 | sylancl 585 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → (𝑧‘𝑚) ∈ 𝐴) |
114 | 97, 110, 113 | fovrnd 7435 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑m suc 𝑚)) → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) ∈ 𝐴) |
115 | 93, 114 | fmpt3d 6984 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)⟶𝐴) |
116 | | elmapi 8611 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝐴 ↑m suc 𝑚) → 𝑎:suc 𝑚⟶𝐴) |
117 | 116 | ad2antrl 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝑎:suc 𝑚⟶𝐴) |
118 | 117 | ffnd 6597 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝑎 Fn suc 𝑚) |
119 | | elmapi 8611 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝐴 ↑m suc 𝑚) → 𝑏:suc 𝑚⟶𝐴) |
120 | 119 | ad2antll 725 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝑏:suc 𝑚⟶𝐴) |
121 | 120 | ffnd 6597 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝑏 Fn suc 𝑚) |
122 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝑚 ⊆ suc 𝑚) |
123 | | fvreseq 6911 |
. . . . . . . . . . . 12
⊢ (((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) ∧ 𝑚 ⊆ suc 𝑚) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥))) |
124 | 118, 121,
122, 123 | syl21anc 834 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥))) |
125 | | fveq2 6768 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑚 → (𝑎‘𝑥) = (𝑎‘𝑚)) |
126 | | fveq2 6768 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑚 → (𝑏‘𝑥) = (𝑏‘𝑚)) |
127 | 125, 126 | eqeq12d 2755 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑚 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚))) |
128 | 54, 127 | ralsn 4622 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑚} (𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚)) |
129 | 128 | bicomi 223 |
. . . . . . . . . . . 12
⊢ ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)) |
130 | 129 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))) |
131 | 124, 130 | anbi12d 630 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))) |
132 | 93 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))) |
133 | 132 | fveq1d 6770 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎)) |
134 | | reseq1 5882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑎 → (𝑧 ↾ 𝑚) = (𝑎 ↾ 𝑚)) |
135 | 134 | fveq2d 6772 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑎 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))) |
136 | | fveq1 6767 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑎 → (𝑧‘𝑚) = (𝑎‘𝑚)) |
137 | 135, 136 | oveq12d 7286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑎 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚))) |
138 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) = (𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) |
139 | | ovex 7301 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) ∈ V |
140 | 137, 138,
139 | fvmpt 6869 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝐴 ↑m suc 𝑚) → ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚))) |
141 | 140 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚))) |
142 | 133, 141 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚))) |
143 | | df-ov 7271 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) = (𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉) |
144 | 142, 143 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉)) |
145 | 132 | fveq1d 6770 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏)) |
146 | | reseq1 5882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑏 → (𝑧 ↾ 𝑚) = (𝑏 ↾ 𝑚)) |
147 | 146 | fveq2d 6772 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑏 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))) |
148 | | fveq1 6767 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑏 → (𝑧‘𝑚) = (𝑏‘𝑚)) |
149 | 147, 148 | oveq12d 7286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑏 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚))) |
150 | | ovex 7301 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) ∈ V |
151 | 149, 138,
150 | fvmpt 6869 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ (𝐴 ↑m suc 𝑚) → ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚))) |
152 | 151 | ad2antll 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚))) |
153 | 145, 152 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚))) |
154 | | df-ov 7271 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉) |
155 | 153, 154 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉)) |
156 | 144, 155 | eqeq12d 2755 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ (𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉))) |
157 | 94 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) |
158 | | f1of1 6711 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)–1-1→𝐴) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1→𝐴) |
160 | 99 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑m 𝑚)⟶𝐴) |
161 | | fssres 6636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑎 ↾ 𝑚):𝑚⟶𝐴) |
162 | 117, 103,
161 | sylancl 585 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑎 ↾ 𝑚):𝑚⟶𝐴) |
163 | 44 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 𝐴 ∈ 𝑉) |
164 | | elmapg 8602 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴)) |
165 | 163, 54, 164 | sylancl 585 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴)) |
166 | 162, 165 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑎 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚)) |
167 | 160, 166 | ffvelrnd 6956 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ 𝐴) |
168 | | ffvelrn 6953 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑎‘𝑚) ∈ 𝐴) |
169 | 117, 111,
168 | sylancl 585 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑎‘𝑚) ∈ 𝐴) |
170 | 167, 169 | opelxpd 5626 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉 ∈ (𝐴 × 𝐴)) |
171 | | fssres 6636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑏 ↾ 𝑚):𝑚⟶𝐴) |
172 | 120, 103,
171 | sylancl 585 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑏 ↾ 𝑚):𝑚⟶𝐴) |
173 | | elmapg 8602 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴)) |
174 | 163, 54, 173 | sylancl 585 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴)) |
175 | 172, 174 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑏 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚)) |
176 | 160, 175 | ffvelrnd 6956 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∈ 𝐴) |
177 | | ffvelrn 6953 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑏‘𝑚) ∈ 𝐴) |
178 | 120, 111,
177 | sylancl 585 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑏‘𝑚) ∈ 𝐴) |
179 | 176, 178 | opelxpd 5626 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → 〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉 ∈ (𝐴 × 𝐴)) |
180 | | f1fveq 7129 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝐴 × 𝐴)–1-1→𝐴 ∧ (〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉 ∈ (𝐴 × 𝐴) ∧ 〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉 ∈ (𝐴 × 𝐴))) → ((𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉) ↔ 〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉 = 〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉)) |
181 | 159, 170,
179, 180 | syl12anc 833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉) ↔ 〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉 = 〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉)) |
182 | | fvex 6781 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ V |
183 | | fvex 6781 |
. . . . . . . . . . . . 13
⊢ (𝑎‘𝑚) ∈ V |
184 | 182, 183 | opth 5393 |
. . . . . . . . . . . 12
⊢
(〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉 = 〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉 ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))) |
185 | 181, 184 | bitrdi 286 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((𝐹‘〈((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)〉) = (𝐹‘〈((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)〉) ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)))) |
186 | | simplrr 774 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴) |
187 | | f1fveq 7129 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴 ∧ ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚) ∧ (𝑏 ↾ 𝑚) ∈ (𝐴 ↑m 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚))) |
188 | 186, 166,
175, 187 | syl12anc 833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚))) |
189 | 188 | anbi1d 629 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → ((((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)))) |
190 | 156, 185,
189 | 3bitrd 304 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)))) |
191 | | eqfnfv 6903 |
. . . . . . . . . . . 12
⊢ ((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥))) |
192 | 118, 121,
191 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥))) |
193 | | df-suc 6269 |
. . . . . . . . . . . . 13
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
194 | 193 | raleqi 3344 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥)) |
195 | | ralunb 4129 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))) |
196 | 194, 195 | bitri 274 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))) |
197 | 192, 196 | bitrdi 286 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (𝑎 = 𝑏 ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))) |
198 | 131, 190,
197 | 3bitr4d 310 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ 𝑎 = 𝑏)) |
199 | 198 | biimpd 228 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)) |
200 | 199 | ralrimivva 3116 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → ∀𝑎 ∈ (𝐴 ↑m suc 𝑚)∀𝑏 ∈ (𝐴 ↑m suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)) |
201 | | dff13 7122 |
. . . . . . 7
⊢ ((𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴 ↔ ((𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)⟶𝐴 ∧ ∀𝑎 ∈ (𝐴 ↑m suc 𝑚)∀𝑏 ∈ (𝐴 ↑m suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))) |
202 | 115, 200,
201 | sylanbrc 582 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴) |
203 | 202 | expr 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ω) → ((𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴)) |
204 | 203 | expcom 413 |
. . . 4
⊢ (𝑚 ∈ ω → (𝜑 → ((𝐺‘𝑚):(𝐴 ↑m 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑m suc 𝑚)–1-1→𝐴))) |
205 | 20, 27, 34, 51, 204 | finds2 7734 |
. . 3
⊢ (𝑦 ∈ ω → (𝜑 → (𝐺‘𝑦):(𝐴 ↑m 𝑦)–1-1→𝐴)) |
206 | 8, 205 | vtoclga 3511 |
. 2
⊢ (𝐶 ∈ ω → (𝜑 → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)) |
207 | 206 | impcom 407 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴) |