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 8742 |
. 2
⊢ (𝜑 → 𝑇 Or 𝑆) |
6 | | oecl 7770 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
7 | 2, 3, 6 | syl2anc 565 |
. . . 4
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ∈ On) |
8 | | eloni 5876 |
. . . 4
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → Ord
(𝐴
↑𝑜 𝐵)) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → Ord (𝐴 ↑𝑜 𝐵)) |
10 | | ordwe 5879 |
. . 3
⊢ (Ord
(𝐴
↑𝑜 𝐵) → E We (𝐴 ↑𝑜 𝐵)) |
11 | | weso 5240 |
. . 3
⊢ ( E We
(𝐴
↑𝑜 𝐵) → E Or (𝐴 ↑𝑜 𝐵)) |
12 | | sopo 5187 |
. . 3
⊢ ( E Or
(𝐴
↑𝑜 𝐵) → E Po (𝐴 ↑𝑜 𝐵)) |
13 | 9, 10, 11, 12 | 4syl 19 |
. 2
⊢ (𝜑 → E Po (𝐴 ↑𝑜 𝐵)) |
14 | 1, 2, 3 | cantnff 8734 |
. . 3
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
15 | | frn 6193 |
. . . . 5
⊢ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) → ran (𝐴 CNF 𝐵) ⊆ (𝐴 ↑𝑜 𝐵)) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴 ↑𝑜 𝐵)) |
17 | | onss 7136 |
. . . . . . . 8
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → (𝐴 ↑𝑜
𝐵) ⊆
On) |
18 | 7, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ⊆ On) |
19 | 18 | sseld 3749 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ On)) |
20 | | eleq1w 2832 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ↔ 𝑦 ∈ (𝐴 ↑𝑜 𝐵))) |
21 | | eleq1w 2832 |
. . . . . . . . . 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 3108 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))) |
25 | | ordelss 5882 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Ord
(𝐴
↑𝑜 𝐵) ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ⊆ (𝐴 ↑𝑜 𝐵)) |
26 | 9, 25 | sylan 561 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ⊆ (𝐴 ↑𝑜 𝐵)) |
27 | 26 | sselda 3750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ (𝐴 ↑𝑜 𝐵)) |
28 | | pm5.5 350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → ((𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) ∧ 𝑦 ∈ 𝑡) → ((𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
30 | 29 | ralbidva 3133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))) |
31 | | dfss3 3739 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)) |
32 | 30, 31 | syl6bbr 278 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) |
33 | | eleq1 2837 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵))) |
34 | 2 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On) |
35 | 34 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On) |
36 | 3 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On) |
37 | 36 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On) |
38 | | simplrl 754 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) |
39 | | simplrr 755 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵)) |
40 | 7 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑𝑜 𝐵) ∈ On) |
41 | | simprl 746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) |
42 | | onelon 5891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → 𝑡 ∈ On) |
43 | 40, 41, 42 | syl2anc 565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On) |
44 | | on0eln0 5923 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ On → (∅
∈ 𝑡 ↔ 𝑡 ≠ ∅)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡 ↔ 𝑡 ≠ ∅)) |
46 | 45 | biimpar 463 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡) |
47 | | eqid 2770 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)} = ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)} |
48 | | eqid 2770 |
. . . . . . . . . . . . . . . . 17
⊢
(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡)) = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡)) |
49 | | eqid 2770 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) = (1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) |
50 | | eqid 2770 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) = (2nd ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑𝑜 𝑐)}) ·𝑜
𝑎) +𝑜
𝑏) = 𝑡))) |
51 | 1, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50 | cantnflem4 8752 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) |
52 | | fczsupp0 7475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 × {∅}) supp
∅) = ∅ |
53 | 52 | eqcomi 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅ =
((𝐵 × {∅}) supp
∅) |
54 | | oieq2 8573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
= ((𝐵 × {∅})
supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅))) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ OrdIso( E
, ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅)) |
56 | | ne0i 4067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐵 → 𝐵 ≠ ∅) |
57 | | ne0i 4067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (𝐴 ↑𝑜 𝐵) ≠ ∅) |
58 | 57 | ad2antrl 699 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑𝑜 𝐵) ≠ ∅) |
59 | | oveq1 6799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
60 | 59 | neeq1d 3001 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵) ≠ ∅ ↔
(∅ ↑𝑜 𝐵) ≠ ∅)) |
61 | 58, 60 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅
↑𝑜 𝐵) ≠ ∅)) |
62 | 61 | necon2d 2965 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅
↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅)) |
63 | | on0eln0 5923 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
64 | | oe0m1 7754 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
65 | 63, 64 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅
↑𝑜 𝐵) = ∅)) |
66 | 36, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅
↑𝑜 𝐵) = ∅)) |
67 | | on0eln0 5923 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
68 | 34, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
69 | 62, 66, 68 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴)) |
70 | 56, 69 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝑦 ∈ 𝐵 → ∅ ∈ 𝐴)) |
71 | 70 | imp 393 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦 ∈ 𝐵) → ∅ ∈ 𝐴) |
72 | | fconstmpt 5303 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 × {∅}) = (𝑦 ∈ 𝐵 ↦ ∅) |
73 | 71, 72 | fmptd 6527 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵⟶𝐴) |
74 | | 0ex 4921 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∅
∈ V |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∅ ∈
V) |
76 | 3, 75 | fczfsuppd 8448 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐵 × {∅}) finSupp
∅) |
77 | 76 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp
∅) |
78 | 1, 2, 3 | cantnfs 8726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
79 | 78 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
80 | 73, 77, 79 | mpbir2and 684 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆) |
81 | | eqid 2770 |
. . . . . . . . . . . . . . . . . . 19
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅) |
82 | 1, 34, 36, 55, 80, 81 | cantnfval 8728 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
(seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 ×
{∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E ,
∅))) |
83 | | we0 5244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ E We
∅ |
84 | | eqid 2770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ OrdIso( E
, ∅) = OrdIso( E , ∅) |
85 | 84 | oien 8598 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((∅
∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈
∅) |
86 | 74, 83, 85 | mp2an 664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ dom
OrdIso( E , ∅) ≈ ∅ |
87 | | en0 8171 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) =
∅) |
88 | 86, 87 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
OrdIso( E , ∅) = ∅ |
89 | 88 | fveq2i 6335 |
. . . . . . . . . . . . . . . . . . 19
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘∅) |
90 | 81 | seqom0g 7703 |
. . . . . . . . . . . . . . . . . . . 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 2792 |
. . . . . . . . . . . . . . . . . 18
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
∅)‘𝑘))
·𝑜 ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+𝑜 𝑧)),
∅)‘dom OrdIso( E , ∅)) = ∅ |
93 | 82, 92 | syl6eq 2820 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) |
94 | 14 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
95 | | ffn 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆) |
97 | | fnfvelrn 6499 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) |
98 | 96, 80, 97 | syl2anc 565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) |
99 | 93, 98 | eqeltrrd 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵)) |
100 | 33, 51, 99 | pm2.61ne 3027 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) |
101 | 100 | expr 444 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
102 | 32, 101 | sylbid 230 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑𝑜 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
103 | 102 | ex 397 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
104 | 103 | com23 86 |
. . . . . . . . . . 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 232 |
. . . . . . . 8
⊢ (𝑡 ∈ On → (∀𝑦 ∈ 𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))) |
108 | 23, 107 | tfis2 7202 |
. . . . . . 7
⊢ (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
109 | 108 | com3l 89 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) |
110 | 19, 109 | mpdd 43 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) |
111 | 110 | ssrdv 3756 |
. . . 4
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵)) |
112 | 16, 111 | eqssd 3767 |
. . 3
⊢ (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴 ↑𝑜 𝐵)) |
113 | | dffo2 6260 |
. . 3
⊢ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴 ↑𝑜 𝐵))) |
114 | 14, 112, 113 | sylanbrc 564 |
. 2
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵)) |
115 | 2 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On) |
116 | 3 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On) |
117 | | fveq2 6332 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑥‘𝑧) = (𝑥‘𝑡)) |
118 | | fveq2 6332 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑦‘𝑧) = (𝑦‘𝑡)) |
119 | 117, 118 | eleq12d 2843 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ↔ (𝑥‘𝑡) ∈ (𝑦‘𝑡))) |
120 | | eleq1w 2832 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤)) |
121 | 120 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
122 | 121 | ralbidv 3134 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
123 | 119, 122 | anbi12d 608 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
124 | 123 | cbvrexv 3320 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
125 | | fveq1 6331 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑥‘𝑡) = (𝑢‘𝑡)) |
126 | | fveq1 6331 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → (𝑦‘𝑡) = (𝑣‘𝑡)) |
127 | | eleq12 2839 |
. . . . . . . . . . . 12
⊢ (((𝑥‘𝑡) = (𝑢‘𝑡) ∧ (𝑦‘𝑡) = (𝑣‘𝑡)) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) |
128 | 125, 126,
127 | syl2an 575 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) |
129 | | fveq1 6331 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (𝑥‘𝑤) = (𝑢‘𝑤)) |
130 | | fveq1 6331 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (𝑦‘𝑤) = (𝑣‘𝑤)) |
131 | 129, 130 | eqeqan12d 2786 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑢‘𝑤) = (𝑣‘𝑤))) |
132 | 131 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) |
133 | 132 | ralbidv 3134 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) |
134 | 128, 133 | anbi12d 608 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
135 | 134 | rexbidv 3199 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
136 | 124, 135 | syl5bb 272 |
. . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) |
137 | 136 | cbvopabv 4854 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} |
138 | 4, 137 | eqtri 2792 |
. . . . . 6
⊢ 𝑇 = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} |
139 | | simprll 756 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓 ∈ 𝑆) |
140 | | simprlr 757 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔 ∈ 𝑆) |
141 | | simprr 748 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔) |
142 | | eqid 2770 |
. . . . . 6
⊢ ∪ {𝑐
∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} = ∪ {𝑐 ∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} |
143 | | eqid 2770 |
. . . . . 6
⊢ OrdIso( E
, (𝑔 supp ∅)) =
OrdIso( E , (𝑔 supp
∅)) |
144 | | eqid 2770 |
. . . . . 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 8749 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) |
146 | | fvex 6342 |
. . . . . 6
⊢ ((𝐴 CNF 𝐵)‘𝑔) ∈ V |
147 | 146 | epelc 5164 |
. . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) |
148 | 145, 147 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)) |
149 | 148 | expr 444 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) |
150 | 149 | ralrimivva 3119 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) |
151 | | soisoi 6720 |
. 2
⊢ (((𝑇 Or 𝑆 ∧ E Po (𝐴 ↑𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑𝑜 𝐵) ∧ ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑𝑜 𝐵))) |
152 | 5, 13, 114, 150, 151 | syl22anc 1476 |
1
⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑𝑜 𝐵))) |