Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
2 | | cantnfs.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | cantnfs.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ On) |
4 | | oemapval.t |
. . 3
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
5 | 1, 2, 3, 4 | oemapso 8462 |
. 2
⊢ (𝜑 → 𝑇 Or 𝑆) |
6 | | oecl 7504 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
7 | 2, 3, 6 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ∈ On) |
8 | | eloni 5650 |
. . . 4
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → Ord
(𝐴
↑𝑜 𝐵)) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → Ord (𝐴 ↑𝑜 𝐵)) |
10 | | ordwe 5653 |
. . 3
⊢ (Ord
(𝐴
↑𝑜 𝐵) → E We (𝐴 ↑𝑜 𝐵)) |
11 | | weso 5029 |
. . 3
⊢ ( E We
(𝐴
↑𝑜 𝐵) → E Or (𝐴 ↑𝑜 𝐵)) |
12 | | sopo 4976 |
. . 3
⊢ ( E Or
(𝐴
↑𝑜 𝐵) → E Po (𝐴 ↑𝑜 𝐵)) |
13 | 9, 10, 11, 12 | 4syl 19 |
. 2
⊢ (𝜑 → E Po (𝐴 ↑𝑜 𝐵)) |
14 | 1, 2, 3 | cantnff 8454 |
. . 3
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
15 | | frn 5966 |
. . . . 5
⊢ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) → ran (𝐴 CNF 𝐵) ⊆ (𝐴 ↑𝑜 𝐵)) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴 ↑𝑜 𝐵)) |
17 | | onss 6882 |
. . . . . . . 8
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → (𝐴 ↑𝑜
𝐵) ⊆
On) |
18 | 7, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ⊆ On) |
19 | 18 | sseld 3567 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ On)) |
20 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ↔ 𝑦 ∈ (𝐴 ↑𝑜 𝐵))) |
21 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
22 | 20, 21 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))) |
23 | 22 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))) |
24 | | r19.21v 2943 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))) |
25 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Ord
(𝐴
↑𝑜 𝐵) ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ⊆ (𝐴 ↑𝑜 𝐵)) |
26 | 9, 25 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ⊆ (𝐴 ↑𝑜 𝐵)) |
27 | 26 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ (𝐴 ↑𝑜 𝐵)) |
28 | | pm5.5 350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → ((𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) ∧ 𝑦 ∈ 𝑡) → ((𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
30 | 29 | ralbidva 2968 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
31 | | dfss3 3558 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)) |
32 | 30, 31 | syl6bbr 277 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) |
33 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵))) |
34 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On) |
36 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On) |
38 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) |
39 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵)) |
40 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑𝑜 𝐵) ∈ On) |
41 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) |
42 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ∈ On) |
43 | 40, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On) |
44 | | on0eln0 5697 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ On → (∅
∈ 𝑡 ↔ 𝑡 ≠ ∅)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡 ↔ 𝑡 ≠ ∅)) |
46 | 45 | biimpar 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡) |
47 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)} = ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)} |
48 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡)) = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡)) |
49 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) = (1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) |
50 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) = (2nd ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) |
51 | 1, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50 | cantnflem4 8472 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) |
52 | | fczsupp0 7211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 × {∅}) supp
∅) = ∅ |
53 | 52 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅ =
((𝐵 × {∅}) supp
∅) |
54 | | oieq2 8301 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
= ((𝐵 × {∅})
supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅))) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ OrdIso( E
, ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅)) |
56 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐵 → 𝐵 ≠ ∅) |
57 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (𝐴 ↑𝑜 𝐵) ≠ ∅) |
58 | 57 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑𝑜 𝐵) ≠ ∅) |
59 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
60 | 59 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵) ≠ ∅ ↔
(∅ ↑𝑜 𝐵) ≠ ∅)) |
61 | 58, 60 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅
↑𝑜 𝐵) ≠ ∅)) |
62 | 61 | necon2d 2805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅
↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅)) |
63 | | on0eln0 5697 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
64 | | oe0m1 7488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
65 | 63, 64 | bitr3d 269 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅
↑𝑜 𝐵) = ∅)) |
66 | 36, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅
↑𝑜 𝐵) = ∅)) |
67 | | on0eln0 5697 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
68 | 34, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
69 | 62, 66, 68 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴)) |
70 | 56, 69 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝑦 ∈ 𝐵 → ∅ ∈ 𝐴)) |
71 | 70 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦 ∈ 𝐵) → ∅ ∈ 𝐴) |
72 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 × {∅}) = (𝑦 ∈ 𝐵 ↦ ∅) |
73 | 71, 72 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵⟶𝐴) |
74 | | 0ex 4718 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∅
∈ V |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∅ ∈
V) |
76 | 3, 75 | fczfsuppd 8176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐵 × {∅}) finSupp
∅) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp
∅) |
78 | 1, 2, 3 | cantnfs 8446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
80 | 73, 77, 79 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆) |
81 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅) |
82 | 1, 34, 36, 55, 80, 81 | cantnfval 8448 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
(seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 ×
{∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E ,
∅))) |
83 | | we0 5033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ E We
∅ |
84 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ OrdIso( E
, ∅) = OrdIso( E , ∅) |
85 | 84 | oien 8326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((∅
∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈
∅) |
86 | 74, 83, 85 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ dom
OrdIso( E , ∅) ≈ ∅ |
87 | | en0 7905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) =
∅) |
88 | 86, 87 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
OrdIso( E , ∅) = ∅ |
89 | 88 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . 19
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘∅) |
90 | 81 | seqom0g 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ V → (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘∅) = ∅) |
91 | 74, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘∅) = ∅ |
92 | 89, 91 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘dom OrdIso( E , ∅)) = ∅ |
93 | 82, 92 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) |
94 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
95 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆) |
97 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) |
98 | 96, 80, 97 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) |
99 | 93, 98 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵)) |
100 | 33, 51, 99 | pm2.61ne 2867 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) |
101 | 100 | expr 641 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
102 | 32, 101 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
103 | 102 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
104 | 103 | com23 84 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
105 | 104 | a2i 14 |
. . . . . . . . . 10
⊢ ((𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
106 | 105 | a1i 11 |
. . . . . . . . 9
⊢ (𝑡 ∈ On → ((𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))) |
107 | 24, 106 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑡 ∈ On → (∀𝑦 ∈ 𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))) |
108 | 23, 107 | tfis2 6948 |
. . . . . . 7
⊢ (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
109 | 108 | com3l 87 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
110 | 19, 109 | mpdd 42 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
111 | 110 | ssrdv 3574 |
. . . 4
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵)) |
112 | 16, 111 | eqssd 3585 |
. . 3
⊢ (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴 ↑𝑜 𝐵)) |
113 | | dffo2 6032 |
. . 3
⊢ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴 ↑𝑜 𝐵))) |
114 | 14, 112, 113 | sylanbrc 695 |
. 2
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵)) |
115 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On) |
116 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On) |
117 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑥‘𝑧) = (𝑥‘𝑡)) |
118 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑦‘𝑧) = (𝑦‘𝑡)) |
119 | 117, 118 | eleq12d 2682 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ↔ (𝑥‘𝑡) ∈ (𝑦‘𝑡))) |
120 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤)) |
121 | 120 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
122 | 121 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
123 | 119, 122 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
124 | 123 | cbvrexv 3148 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
125 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑥‘𝑡) = (𝑢‘𝑡)) |
126 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → (𝑦‘𝑡) = (𝑣‘𝑡)) |
127 | | eleq12 2678 |
. . . . . . . . . . . 12
⊢ (((𝑥‘𝑡) = (𝑢‘𝑡) ∧ (𝑦‘𝑡) = (𝑣‘𝑡)) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) |
128 | 125, 126,
127 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) |
129 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (𝑥‘𝑤) = (𝑢‘𝑤)) |
130 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (𝑦‘𝑤) = (𝑣‘𝑤)) |
131 | 129, 130 | eqeqan12d 2626 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑢‘𝑤) = (𝑣‘𝑤))) |
132 | 131 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) |
133 | 132 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) |
134 | 128, 133 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
135 | 134 | rexbidv 3034 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
136 | 124, 135 | syl5bb 271 |
. . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
137 | 136 | cbvopabv 4654 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} |
138 | 4, 137 | eqtri 2632 |
. . . . . 6
⊢ 𝑇 = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} |
139 | | simprll 798 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓 ∈ 𝑆) |
140 | | simprlr 799 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔 ∈ 𝑆) |
141 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔) |
142 | | eqid 2610 |
. . . . . 6
⊢ ∪ {𝑐
∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} = ∪ {𝑐 ∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} |
143 | | eqid 2610 |
. . . . . 6
⊢ OrdIso( E
, (𝑔 supp ∅)) =
OrdIso( E , (𝑔 supp
∅)) |
144 | | eqid 2610 |
. . . . . 6
⊢
seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑔 supp
∅))‘𝑘))
·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅) = seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑔 supp
∅))‘𝑘))
·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅) |
145 | 1, 115, 116, 138, 139, 140, 141, 142, 143, 144 | cantnflem1 8469 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) |
146 | | fvex 6113 |
. . . . . 6
⊢ ((𝐴 CNF 𝐵)‘𝑔) ∈ V |
147 | 146 | epelc 4951 |
. . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) |
148 | 145, 147 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)) |
149 | 148 | expr 641 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) |
150 | 149 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) |
151 | | soisoi 6478 |
. 2
⊢ (((𝑇 Or 𝑆 ∧ E Po (𝐴 ↑𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵) ∧ ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑𝑜 𝐵))) |
152 | 5, 13, 114, 150, 151 | syl22anc 1319 |
1
⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑𝑜 𝐵))) |