| 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 9722 | . 2
⊢ (𝜑 → 𝑇 Or 𝑆) | 
| 6 |  | oecl 8575 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) | 
| 7 | 2, 3, 6 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐴 ↑o 𝐵) ∈ On) | 
| 8 |  | eloni 6394 | . . . 4
⊢ ((𝐴 ↑o 𝐵) ∈ On → Ord (𝐴 ↑o 𝐵)) | 
| 9 | 7, 8 | syl 17 | . . 3
⊢ (𝜑 → Ord (𝐴 ↑o 𝐵)) | 
| 10 |  | ordwe 6397 | . . 3
⊢ (Ord
(𝐴 ↑o 𝐵) → E We (𝐴 ↑o 𝐵)) | 
| 11 |  | weso 5676 | . . 3
⊢ ( E We
(𝐴 ↑o 𝐵) → E Or (𝐴 ↑o 𝐵)) | 
| 12 |  | sopo 5611 | . . 3
⊢ ( E Or
(𝐴 ↑o 𝐵) → E Po (𝐴 ↑o 𝐵)) | 
| 13 | 9, 10, 11, 12 | 4syl 19 | . 2
⊢ (𝜑 → E Po (𝐴 ↑o 𝐵)) | 
| 14 | 1, 2, 3 | cantnff 9714 | . . 3
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵)) | 
| 15 | 14 | frnd 6744 | . . . 4
⊢ (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴 ↑o 𝐵)) | 
| 16 |  | onss 7805 | . . . . . . . 8
⊢ ((𝐴 ↑o 𝐵) ∈ On → (𝐴 ↑o 𝐵) ⊆ On) | 
| 17 | 7, 16 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐴 ↑o 𝐵) ⊆ On) | 
| 18 | 17 | sseld 3982 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ On)) | 
| 19 |  | eleq1w 2824 | . . . . . . . . . 10
⊢ (𝑡 = 𝑦 → (𝑡 ∈ (𝐴 ↑o 𝐵) ↔ 𝑦 ∈ (𝐴 ↑o 𝐵))) | 
| 20 |  | eleq1w 2824 | . . . . . . . . . 10
⊢ (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) | 
| 21 | 19, 20 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))) | 
| 22 | 21 | imbi2d 340 | . . . . . . . 8
⊢ (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))) | 
| 23 |  | r19.21v 3180 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))) | 
| 24 |  | ordelss 6400 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Ord
(𝐴 ↑o 𝐵) ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → 𝑡 ⊆ (𝐴 ↑o 𝐵)) | 
| 25 | 9, 24 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → 𝑡 ⊆ (𝐴 ↑o 𝐵)) | 
| 26 | 25 | sselda 3983 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ (𝐴 ↑o 𝐵)) | 
| 27 |  | pm5.5 361 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝐴 ↑o 𝐵) → ((𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) ∧ 𝑦 ∈ 𝑡) → ((𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵))) | 
| 29 | 28 | ralbidva 3176 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))) | 
| 30 |  | dfss3 3972 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)) | 
| 31 | 29, 30 | bitr4di 289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) | 
| 32 |  | eleq1 2829 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵))) | 
| 33 | 2 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On) | 
| 35 | 3 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On) | 
| 37 |  | simplrl 777 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴 ↑o 𝐵)) | 
| 38 |  | simplrr 778 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵)) | 
| 39 | 7 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑o 𝐵) ∈ On) | 
| 40 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴 ↑o 𝐵)) | 
| 41 |  | onelon 6409 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ↑o 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → 𝑡 ∈ On) | 
| 42 | 39, 40, 41 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On) | 
| 43 |  | on0eln0 6440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ On → (∅
∈ 𝑡 ↔ 𝑡 ≠ ∅)) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡 ↔ 𝑡 ≠ ∅)) | 
| 45 | 44 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡) | 
| 46 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)} = ∪ ∩ {𝑐
∈ On ∣ 𝑡 ∈
(𝐴 ↑o 𝑐)} | 
| 47 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)) = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)) | 
| 48 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))) = (1st ‘(℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)})(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴 ↑o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))) | 
| 49 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(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 9732 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) | 
| 51 |  | fczsupp0 8218 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 × {∅}) supp
∅) = ∅ | 
| 52 | 51 | eqcomi 2746 | . . . . . . . . . . . . . . . . . . . 20
⊢ ∅ =
((𝐵 × {∅}) supp
∅) | 
| 53 |  | oieq2 9553 | . . . . . . . . . . . . . . . . . . . 20
⊢ (∅
= ((𝐵 × {∅})
supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅))) | 
| 54 | 52, 53 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ OrdIso( E
, ∅) = OrdIso( E , ((𝐵 × {∅}) supp
∅)) | 
| 55 |  | ne0i 4341 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ (𝐴 ↑o 𝐵) → (𝐴 ↑o 𝐵) ≠ ∅) | 
| 56 | 55 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 ↑o 𝐵) ≠ ∅) | 
| 57 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) | 
| 58 | 57 | neeq1d 3000 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) ≠ ∅ ↔ (∅
↑o 𝐵) ≠
∅)) | 
| 59 | 56, 58 | syl5ibcom 245 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅
↑o 𝐵) ≠
∅)) | 
| 60 | 59 | necon2d 2963 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑o
𝐵) = ∅ → 𝐴 ≠ ∅)) | 
| 61 |  | on0eln0 6440 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) | 
| 62 |  | oe0m1 8559 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) | 
| 63 | 61, 62 | bitr3d 281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅
↑o 𝐵) =
∅)) | 
| 64 | 35, 63 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅
↑o 𝐵) =
∅)) | 
| 65 |  | on0eln0 6440 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 66 | 33, 65 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 67 | 60, 64, 66 | 3imtr4d 294 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴)) | 
| 68 |  | ne0i 4341 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐵 → 𝐵 ≠ ∅) | 
| 69 | 67, 68 | impel 505 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦 ∈ 𝐵) → ∅ ∈ 𝐴) | 
| 70 |  | fconstmpt 5747 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 × {∅}) = (𝑦 ∈ 𝐵 ↦ ∅) | 
| 71 | 69, 70 | fmptd 7134 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵⟶𝐴) | 
| 72 |  | 0ex 5307 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∅
∈ V | 
| 73 | 72 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∅ ∈
V) | 
| 74 | 3, 73 | fczfsuppd 9426 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐵 × {∅}) finSupp
∅) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp
∅) | 
| 76 | 1, 2, 3 | cantnfs 9706 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) | 
| 77 | 76 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) | 
| 78 | 71, 75, 77 | mpbir2and 713 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆) | 
| 79 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢
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 9708 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E ,
∅)‘𝑘)))
+o 𝑧)),
∅)‘dom OrdIso( E , ∅))) | 
| 81 |  | we0 5680 | . . . . . . . . . . . . . . . . . . . . . 22
⊢  E We
∅ | 
| 82 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ OrdIso( E
, ∅) = OrdIso( E , ∅) | 
| 83 | 82 | oien 9578 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((∅
∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈
∅) | 
| 84 | 72, 81, 83 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . 21
⊢ dom
OrdIso( E , ∅) ≈ ∅ | 
| 85 |  | en0 9058 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) =
∅) | 
| 86 | 84, 85 | mpbi 230 | . . . . . . . . . . . . . . . . . . . 20
⊢ dom
OrdIso( E , ∅) = ∅ | 
| 87 | 86 | fveq2i 6909 | . . . . . . . . . . . . . . . . . . 19
⊢
(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 8496 | . . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ V → (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E ,
∅)‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅) | 
| 89 | 72, 88 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E ,
∅)‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅ | 
| 90 | 87, 89 | eqtri 2765 | . . . . . . . . . . . . . . . . . 18
⊢
(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E ,
∅)‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅))
= ∅ | 
| 91 | 80, 90 | eqtrdi 2793 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) | 
| 92 | 14 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵)) | 
| 93 | 92 | ffnd 6737 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆) | 
| 94 |  | fnfvelrn 7100 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) | 
| 95 | 93, 78, 94 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵)) | 
| 96 | 91, 95 | eqeltrrd 2842 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵)) | 
| 97 | 32, 50, 96 | pm2.61ne 3027 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑡 ∈ (𝐴 ↑o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) | 
| 98 | 97 | expr 456 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) | 
| 99 | 31, 98 | sylbid 240 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴 ↑o 𝐵)) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) | 
| 100 | 99 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) | 
| 101 | 100 | com23 86 | . . . . . . . . . . 11
⊢ (𝜑 → (∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) | 
| 102 | 101 | a2i 14 | . . . . . . . . . 10
⊢ ((𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) | 
| 103 | 102 | a1i 11 | . . . . . . . . 9
⊢ (𝑡 ∈ On → ((𝜑 → ∀𝑦 ∈ 𝑡 (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))) | 
| 104 | 23, 103 | biimtrid 242 | . . . . . . . 8
⊢ (𝑡 ∈ On → (∀𝑦 ∈ 𝑡 (𝜑 → (𝑦 ∈ (𝐴 ↑o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))) | 
| 105 | 22, 104 | tfis2 7878 | . . . . . . 7
⊢ (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) | 
| 106 | 105 | com3l 89 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵)))) | 
| 107 | 18, 106 | mpdd 43 | . . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴 ↑o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) | 
| 108 | 107 | ssrdv 3989 | . . . 4
⊢ (𝜑 → (𝐴 ↑o 𝐵) ⊆ ran (𝐴 CNF 𝐵)) | 
| 109 | 15, 108 | eqssd 4001 | . . 3
⊢ (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴 ↑o 𝐵)) | 
| 110 |  | dffo2 6824 | . . 3
⊢ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑o 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴 ↑o 𝐵))) | 
| 111 | 14, 109, 110 | sylanbrc 583 | . 2
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑o 𝐵)) | 
| 112 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On) | 
| 113 | 3 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On) | 
| 114 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑥‘𝑧) = (𝑥‘𝑡)) | 
| 115 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝑦‘𝑧) = (𝑦‘𝑡)) | 
| 116 | 114, 115 | eleq12d 2835 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ↔ (𝑥‘𝑡) ∈ (𝑦‘𝑡))) | 
| 117 |  | eleq1w 2824 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤)) | 
| 118 | 117 | imbi1d 341 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 119 | 118 | ralbidv 3178 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 120 | 116, 119 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) | 
| 121 | 120 | cbvrexvw 3238 | . . . . . . . . 9
⊢
(∃𝑧 ∈
𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 122 |  | fveq1 6905 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (𝑥‘𝑡) = (𝑢‘𝑡)) | 
| 123 |  | fveq1 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → (𝑦‘𝑡) = (𝑣‘𝑡)) | 
| 124 |  | eleq12 2831 | . . . . . . . . . . . 12
⊢ (((𝑥‘𝑡) = (𝑢‘𝑡) ∧ (𝑦‘𝑡) = (𝑣‘𝑡)) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) | 
| 125 | 122, 123,
124 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ↔ (𝑢‘𝑡) ∈ (𝑣‘𝑡))) | 
| 126 |  | fveq1 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (𝑥‘𝑤) = (𝑢‘𝑤)) | 
| 127 |  | fveq1 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (𝑦‘𝑤) = (𝑣‘𝑤)) | 
| 128 | 126, 127 | eqeqan12d 2751 | . . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑢‘𝑤) = (𝑣‘𝑤))) | 
| 129 | 128 | imbi2d 340 | . . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) | 
| 130 | 129 | ralbidv 3178 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))) | 
| 131 | 125, 130 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) | 
| 132 | 131 | rexbidv 3179 | . . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑡 ∈ 𝐵 ((𝑥‘𝑡) ∈ (𝑦‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) | 
| 133 | 121, 132 | bitrid 283 | . . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤))))) | 
| 134 | 133 | cbvopabv 5216 | . . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} | 
| 135 | 4, 134 | eqtri 2765 | . . . . . 6
⊢ 𝑇 = {〈𝑢, 𝑣〉 ∣ ∃𝑡 ∈ 𝐵 ((𝑢‘𝑡) ∈ (𝑣‘𝑡) ∧ ∀𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 → (𝑢‘𝑤) = (𝑣‘𝑤)))} | 
| 136 |  | simprll 779 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓 ∈ 𝑆) | 
| 137 |  | simprlr 780 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔 ∈ 𝑆) | 
| 138 |  | simprr 773 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔) | 
| 139 |  | eqid 2737 | . . . . . 6
⊢ ∪ {𝑐
∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} = ∪ {𝑐 ∈ 𝐵 ∣ (𝑓‘𝑐) ∈ (𝑔‘𝑐)} | 
| 140 |  | eqid 2737 | . . . . . 6
⊢ OrdIso( E
, (𝑔 supp ∅)) =
OrdIso( E , (𝑔 supp
∅)) | 
| 141 |  | eqid 2737 | . . . . . 6
⊢
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 9729 | . . . . 5
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) | 
| 143 |  | fvex 6919 | . . . . . 6
⊢ ((𝐴 CNF 𝐵)‘𝑔) ∈ V | 
| 144 | 143 | epeli 5586 | . . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔)) | 
| 145 | 142, 144 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)) | 
| 146 | 145 | expr 456 | . . 3
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) | 
| 147 | 146 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))) | 
| 148 |  | soisoi 7348 | . 2
⊢ (((𝑇 Or 𝑆 ∧ E Po (𝐴 ↑o 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆–onto→(𝐴 ↑o 𝐵) ∧ ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵))) | 
| 149 | 5, 13, 111, 147, 148 | syl22anc 839 | 1
⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵))) |