Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
oemapval.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
5 |
1 2 3 4
|
oemapso |
⊢ ( 𝜑 → 𝑇 Or 𝑆 ) |
6 |
|
oecl |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
7 |
2 3 6
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
8 |
|
eloni |
⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) ) |
9 |
7 8
|
syl |
⊢ ( 𝜑 → Ord ( 𝐴 ↑o 𝐵 ) ) |
10 |
|
ordwe |
⊢ ( Ord ( 𝐴 ↑o 𝐵 ) → E We ( 𝐴 ↑o 𝐵 ) ) |
11 |
|
weso |
⊢ ( E We ( 𝐴 ↑o 𝐵 ) → E Or ( 𝐴 ↑o 𝐵 ) ) |
12 |
|
sopo |
⊢ ( E Or ( 𝐴 ↑o 𝐵 ) → E Po ( 𝐴 ↑o 𝐵 ) ) |
13 |
9 10 11 12
|
4syl |
⊢ ( 𝜑 → E Po ( 𝐴 ↑o 𝐵 ) ) |
14 |
1 2 3
|
cantnff |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) ) |
15 |
14
|
frnd |
⊢ ( 𝜑 → ran ( 𝐴 CNF 𝐵 ) ⊆ ( 𝐴 ↑o 𝐵 ) ) |
16 |
|
onss |
⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → ( 𝐴 ↑o 𝐵 ) ⊆ On ) |
17 |
7 16
|
syl |
⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ⊆ On ) |
18 |
17
|
sseld |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ On ) ) |
19 |
|
eleq1w |
⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) ) ) |
20 |
|
eleq1w |
⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
21 |
19 20
|
imbi12d |
⊢ ( 𝑡 = 𝑦 → ( ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
22 |
21
|
imbi2d |
⊢ ( 𝑡 = 𝑦 → ( ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) ) |
23 |
|
r19.21v |
⊢ ( ∀ 𝑦 ∈ 𝑡 ( 𝜑 → ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
24 |
|
ordelss |
⊢ ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → 𝑡 ⊆ ( 𝐴 ↑o 𝐵 ) ) |
25 |
9 24
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → 𝑡 ⊆ ( 𝐴 ↑o 𝐵 ) ) |
26 |
25
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) ∧ 𝑦 ∈ 𝑡 ) → 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) ) |
27 |
|
pm5.5 |
⊢ ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → ( ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
28 |
26 27
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) ∧ 𝑦 ∈ 𝑡 ) → ( ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
29 |
28
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ ∀ 𝑦 ∈ 𝑡 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
30 |
|
dfss3 |
⊢ ( 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑡 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) |
31 |
29 30
|
bitr4di |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) |
32 |
|
eleq1 |
⊢ ( 𝑡 = ∅ → ( 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ ∅ ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
33 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝐴 ∈ On ) |
34 |
33
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝐴 ∈ On ) |
35 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝐵 ∈ On ) |
36 |
35
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝐵 ∈ On ) |
37 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) |
38 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) |
39 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 ↑o 𝐵 ) ∈ On ) |
40 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) |
41 |
|
onelon |
⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → 𝑡 ∈ On ) |
42 |
39 40 41
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ On ) |
43 |
|
on0eln0 |
⊢ ( 𝑡 ∈ On → ( ∅ ∈ 𝑡 ↔ 𝑡 ≠ ∅ ) ) |
44 |
42 43
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ∅ ∈ 𝑡 ↔ 𝑡 ≠ ∅ ) ) |
45 |
44
|
biimpar |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → ∅ ∈ 𝑡 ) |
46 |
|
eqid |
⊢ ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } = ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } |
47 |
|
eqid |
⊢ ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) = ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) |
48 |
|
eqid |
⊢ ( 1st ‘ ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) = ( 1st ‘ ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) |
49 |
|
eqid |
⊢ ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) = ( 2nd ‘ ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ( 𝑑 = 〈 𝑎 , 𝑏 〉 ∧ ( ( ( 𝐴 ↑o ∪ ∩ { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴 ↑o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) |
50 |
1 34 36 4 37 38 45 46 47 48 49
|
cantnflem4 |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) |
51 |
|
fczsupp0 |
⊢ ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅ |
52 |
51
|
eqcomi |
⊢ ∅ = ( ( 𝐵 × { ∅ } ) supp ∅ ) |
53 |
|
oieq2 |
⊢ ( ∅ = ( ( 𝐵 × { ∅ } ) supp ∅ ) → OrdIso ( E , ∅ ) = OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ) |
54 |
52 53
|
ax-mp |
⊢ OrdIso ( E , ∅ ) = OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) |
55 |
|
ne0i |
⊢ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → ( 𝐴 ↑o 𝐵 ) ≠ ∅ ) |
56 |
55
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 ↑o 𝐵 ) ≠ ∅ ) |
57 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) ) |
58 |
57
|
neeq1d |
⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) ≠ ∅ ) ) |
59 |
56 58
|
syl5ibcom |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 = ∅ → ( ∅ ↑o 𝐵 ) ≠ ∅ ) ) |
60 |
59
|
necon2d |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( ∅ ↑o 𝐵 ) = ∅ → 𝐴 ≠ ∅ ) ) |
61 |
|
on0eln0 |
⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) ) |
62 |
|
oe0m1 |
⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
63 |
61 62
|
bitr3d |
⊢ ( 𝐵 ∈ On → ( 𝐵 ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
64 |
35 63
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
65 |
|
on0eln0 |
⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
66 |
33 65
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
67 |
60 64 66
|
3imtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 ≠ ∅ → ∅ ∈ 𝐴 ) ) |
68 |
|
ne0i |
⊢ ( 𝑦 ∈ 𝐵 → 𝐵 ≠ ∅ ) |
69 |
67 68
|
impel |
⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ 𝐴 ) |
70 |
|
fconstmpt |
⊢ ( 𝐵 × { ∅ } ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) |
71 |
69 70
|
fmptd |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 ) |
72 |
|
0ex |
⊢ ∅ ∈ V |
73 |
72
|
a1i |
⊢ ( 𝜑 → ∅ ∈ V ) |
74 |
3 73
|
fczfsuppd |
⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) finSupp ∅ ) |
75 |
74
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) finSupp ∅ ) |
76 |
1 2 3
|
cantnfs |
⊢ ( 𝜑 → ( ( 𝐵 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) ) |
77 |
76
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐵 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) ) |
78 |
71 75 77
|
mpbir2and |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) ∈ 𝑆 ) |
79 |
|
eqid |
⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) |
80 |
1 33 35 54 78 79
|
cantnfval |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) ) |
81 |
|
we0 |
⊢ E We ∅ |
82 |
|
eqid |
⊢ OrdIso ( E , ∅ ) = OrdIso ( E , ∅ ) |
83 |
82
|
oien |
⊢ ( ( ∅ ∈ V ∧ E We ∅ ) → dom OrdIso ( E , ∅ ) ≈ ∅ ) |
84 |
72 81 83
|
mp2an |
⊢ dom OrdIso ( E , ∅ ) ≈ ∅ |
85 |
|
en0 |
⊢ ( dom OrdIso ( E , ∅ ) ≈ ∅ ↔ dom OrdIso ( E , ∅ ) = ∅ ) |
86 |
84 85
|
mpbi |
⊢ dom OrdIso ( E , ∅ ) = ∅ |
87 |
86
|
fveq2i |
⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) |
88 |
79
|
seqom0g |
⊢ ( ∅ ∈ V → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ ) |
89 |
72 88
|
ax-mp |
⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ |
90 |
87 89
|
eqtri |
⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) = ∅ |
91 |
80 90
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ ) |
92 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) ) |
93 |
92
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 CNF 𝐵 ) Fn 𝑆 ) |
94 |
|
fnfvelrn |
⊢ ( ( ( 𝐴 CNF 𝐵 ) Fn 𝑆 ∧ ( 𝐵 × { ∅ } ) ∈ 𝑆 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ∈ ran ( 𝐴 CNF 𝐵 ) ) |
95 |
93 78 94
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ∈ ran ( 𝐴 CNF 𝐵 ) ) |
96 |
91 95
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ∅ ∈ ran ( 𝐴 CNF 𝐵 ) ) |
97 |
32 50 96
|
pm2.61ne |
⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) |
98 |
97
|
expr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
99 |
31 98
|
sylbid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
100 |
99
|
ex |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → ( ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
101 |
100
|
com23 |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
102 |
101
|
a2i |
⊢ ( ( 𝜑 → ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
103 |
102
|
a1i |
⊢ ( 𝑡 ∈ On → ( ( 𝜑 → ∀ 𝑦 ∈ 𝑡 ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) ) |
104 |
23 103
|
syl5bi |
⊢ ( 𝑡 ∈ On → ( ∀ 𝑦 ∈ 𝑡 ( 𝜑 → ( 𝑦 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) ) |
105 |
22 104
|
tfis2 |
⊢ ( 𝑡 ∈ On → ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
106 |
105
|
com3l |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → ( 𝑡 ∈ On → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) |
107 |
18 106
|
mpdd |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 ↑o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) |
108 |
107
|
ssrdv |
⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ⊆ ran ( 𝐴 CNF 𝐵 ) ) |
109 |
15 108
|
eqssd |
⊢ ( 𝜑 → ran ( 𝐴 CNF 𝐵 ) = ( 𝐴 ↑o 𝐵 ) ) |
110 |
|
dffo2 |
⊢ ( ( 𝐴 CNF 𝐵 ) : 𝑆 –onto→ ( 𝐴 ↑o 𝐵 ) ↔ ( ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) ∧ ran ( 𝐴 CNF 𝐵 ) = ( 𝐴 ↑o 𝐵 ) ) ) |
111 |
14 109 110
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 –onto→ ( 𝐴 ↑o 𝐵 ) ) |
112 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝐴 ∈ On ) |
113 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝐵 ∈ On ) |
114 |
|
fveq2 |
⊢ ( 𝑧 = 𝑡 → ( 𝑥 ‘ 𝑧 ) = ( 𝑥 ‘ 𝑡 ) ) |
115 |
|
fveq2 |
⊢ ( 𝑧 = 𝑡 → ( 𝑦 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑡 ) ) |
116 |
114 115
|
eleq12d |
⊢ ( 𝑧 = 𝑡 → ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ↔ ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ) ) |
117 |
|
eleq1w |
⊢ ( 𝑧 = 𝑡 → ( 𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤 ) ) |
118 |
117
|
imbi1d |
⊢ ( 𝑧 = 𝑡 → ( ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) |
119 |
118
|
ralbidv |
⊢ ( 𝑧 = 𝑡 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) |
120 |
116 119
|
anbi12d |
⊢ ( 𝑧 = 𝑡 → ( ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) ) |
121 |
120
|
cbvrexvw |
⊢ ( ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) |
122 |
|
fveq1 |
⊢ ( 𝑥 = 𝑢 → ( 𝑥 ‘ 𝑡 ) = ( 𝑢 ‘ 𝑡 ) ) |
123 |
|
fveq1 |
⊢ ( 𝑦 = 𝑣 → ( 𝑦 ‘ 𝑡 ) = ( 𝑣 ‘ 𝑡 ) ) |
124 |
|
eleq12 |
⊢ ( ( ( 𝑥 ‘ 𝑡 ) = ( 𝑢 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) = ( 𝑣 ‘ 𝑡 ) ) → ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ↔ ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ) ) |
125 |
122 123 124
|
syl2an |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ↔ ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ) ) |
126 |
|
fveq1 |
⊢ ( 𝑥 = 𝑢 → ( 𝑥 ‘ 𝑤 ) = ( 𝑢 ‘ 𝑤 ) ) |
127 |
|
fveq1 |
⊢ ( 𝑦 = 𝑣 → ( 𝑦 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) |
128 |
126 127
|
eqeqan12d |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ↔ ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) |
129 |
128
|
imbi2d |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) |
130 |
129
|
ralbidv |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) |
131 |
125 130
|
anbi12d |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) ) |
132 |
131
|
rexbidv |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑥 ‘ 𝑡 ) ∈ ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) ) |
133 |
121 132
|
syl5bb |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) ) |
134 |
133
|
cbvopabv |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } = { 〈 𝑢 , 𝑣 〉 ∣ ∃ 𝑡 ∈ 𝐵 ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) } |
135 |
4 134
|
eqtri |
⊢ 𝑇 = { 〈 𝑢 , 𝑣 〉 ∣ ∃ 𝑡 ∈ 𝐵 ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) } |
136 |
|
simprll |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑓 ∈ 𝑆 ) |
137 |
|
simprlr |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑔 ∈ 𝑆 ) |
138 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑓 𝑇 𝑔 ) |
139 |
|
eqid |
⊢ ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑔 ‘ 𝑐 ) } = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝑓 ‘ 𝑐 ) ∈ ( 𝑔 ‘ 𝑐 ) } |
140 |
|
eqid |
⊢ OrdIso ( E , ( 𝑔 supp ∅ ) ) = OrdIso ( E , ( 𝑔 supp ∅ ) ) |
141 |
|
eqid |
⊢ seqω ( ( 𝑘 ∈ V , 𝑡 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑔 ‘ ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑡 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑡 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑔 ‘ ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑡 ) ) , ∅ ) |
142 |
1 112 113 135 136 137 138 139 140 141
|
cantnflem1 |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) |
143 |
|
fvex |
⊢ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ∈ V |
144 |
143
|
epeli |
⊢ ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) |
145 |
142 144
|
sylibr |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) |
146 |
145
|
expr |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ) → ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) ) |
147 |
146
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑆 ∀ 𝑔 ∈ 𝑆 ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) ) |
148 |
|
soisoi |
⊢ ( ( ( 𝑇 Or 𝑆 ∧ E Po ( 𝐴 ↑o 𝐵 ) ) ∧ ( ( 𝐴 CNF 𝐵 ) : 𝑆 –onto→ ( 𝐴 ↑o 𝐵 ) ∧ ∀ 𝑓 ∈ 𝑆 ∀ 𝑔 ∈ 𝑆 ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) ) ) → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) ) |
149 |
5 13 111 147 148
|
syl22anc |
⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) ) |