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