| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cantnfs.b | . . 3
⊢ (𝜑 → 𝐵 ∈ On) | 
| 2 |  | eloni 6394 | . . . . 5
⊢ (𝐵 ∈ On → Ord 𝐵) | 
| 3 |  | ordwe 6397 | . . . . 5
⊢ (Ord
𝐵 → E We 𝐵) | 
| 4 |  | weso 5676 | . . . . 5
⊢ ( E We
𝐵 → E Or 𝐵) | 
| 5 | 1, 2, 3, 4 | 4syl 19 | . . . 4
⊢ (𝜑 → E Or 𝐵) | 
| 6 |  | cnvso 6308 | . . . 4
⊢ ( E Or
𝐵 ↔ ◡ E Or 𝐵) | 
| 7 | 5, 6 | sylib 218 | . . 3
⊢ (𝜑 → ◡ E Or 𝐵) | 
| 8 |  | cantnfs.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ On) | 
| 9 |  | eloni 6394 | . . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) | 
| 10 |  | ordwe 6397 | . . . 4
⊢ (Ord
𝐴 → E We 𝐴) | 
| 11 |  | weso 5676 | . . . 4
⊢ ( E We
𝐴 → E Or 𝐴) | 
| 12 | 8, 9, 10, 11 | 4syl 19 | . . 3
⊢ (𝜑 → E Or 𝐴) | 
| 13 |  | oemapval.t | . . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} | 
| 14 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝑦‘𝑧) ∈ V | 
| 15 | 14 | epeli 5586 | . . . . . . . 8
⊢ ((𝑥‘𝑧) E (𝑦‘𝑧) ↔ (𝑥‘𝑧) ∈ (𝑦‘𝑧)) | 
| 16 |  | vex 3484 | . . . . . . . . . . . 12
⊢ 𝑤 ∈ V | 
| 17 |  | vex 3484 | . . . . . . . . . . . 12
⊢ 𝑧 ∈ V | 
| 18 | 16, 17 | brcnv 5893 | . . . . . . . . . . 11
⊢ (𝑤◡ E 𝑧 ↔ 𝑧 E 𝑤) | 
| 19 |  | epel 5587 | . . . . . . . . . . 11
⊢ (𝑧 E 𝑤 ↔ 𝑧 ∈ 𝑤) | 
| 20 | 18, 19 | bitri 275 | . . . . . . . . . 10
⊢ (𝑤◡ E 𝑧 ↔ 𝑧 ∈ 𝑤) | 
| 21 | 20 | imbi1i 349 | . . . . . . . . 9
⊢ ((𝑤◡ E 𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) | 
| 22 | 21 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑤 ∈
𝐵 (𝑤◡ E
𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) | 
| 23 | 15, 22 | anbi12i 628 | . . . . . . 7
⊢ (((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑤◡ E
𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 24 | 23 | rexbii 3094 | . . . . . 6
⊢
(∃𝑧 ∈
𝐵 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑤◡ E
𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 25 | 24 | opabbii 5210 | . . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑤◡ E
𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} | 
| 26 | 13, 25 | eqtr4i 2768 | . . . 4
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑤◡ E
𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} | 
| 27 |  | breq1 5146 | . . . . 5
⊢ (𝑔 = 𝑥 → (𝑔 finSupp ∅ ↔ 𝑥 finSupp ∅)) | 
| 28 | 27 | cbvrabv 3447 | . . . 4
⊢ {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} | 
| 29 | 26, 28 | wemapso2 9593 | . . 3
⊢ ((𝐵 ∈ On ∧ ◡ E Or 𝐵 ∧ E Or 𝐴) → 𝑇 Or {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) | 
| 30 | 1, 7, 12, 29 | syl3anc 1373 | . 2
⊢ (𝜑 → 𝑇 Or {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) | 
| 31 |  | cantnfs.s | . . . 4
⊢ 𝑆 = dom (𝐴 CNF 𝐵) | 
| 32 |  | eqid 2737 | . . . . 5
⊢ {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} | 
| 33 | 32, 8, 1 | cantnfdm 9704 | . . . 4
⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) | 
| 34 | 31, 33 | eqtrid 2789 | . . 3
⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) | 
| 35 |  | soeq2 5614 | . . 3
⊢ (𝑆 = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} → (𝑇 Or 𝑆 ↔ 𝑇 Or {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅})) | 
| 36 | 34, 35 | syl 17 | . 2
⊢ (𝜑 → (𝑇 Or 𝑆 ↔ 𝑇 Or {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅})) | 
| 37 | 30, 36 | mpbird 257 | 1
⊢ (𝜑 → 𝑇 Or 𝑆) |