Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
eqid |
⊢ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } |
5 |
4 2 3
|
cantnfdm |
⊢ ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) |
6 |
1 5
|
eqtrid |
⊢ ( 𝜑 → 𝑆 = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) |
7 |
6
|
eleq2d |
⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) ) |
8 |
|
breq1 |
⊢ ( 𝑔 = 𝐹 → ( 𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅ ) ) |
9 |
8
|
elrab |
⊢ ( 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↔ ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ) |
10 |
7 9
|
bitrdi |
⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ) ) |
11 |
2 3
|
elmapd |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐴 ) ) |
12 |
11
|
anbi1d |
⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) ) |
13 |
10 12
|
bitrd |
⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) ) |