Proof of Theorem intopsn
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ⚬ :(𝐵 × 𝐵)⟶𝐵) |
2 | | id 22 |
. . . . . 6
⊢ (𝐵 = {𝑍} → 𝐵 = {𝑍}) |
3 | 2 | sqxpeqd 5617 |
. . . . 5
⊢ (𝐵 = {𝑍} → (𝐵 × 𝐵) = ({𝑍} × {𝑍})) |
4 | 3, 2 | feq23d 6588 |
. . . 4
⊢ (𝐵 = {𝑍} → ( ⚬ :(𝐵 × 𝐵)⟶𝐵 ↔ ⚬ :({𝑍} × {𝑍})⟶{𝑍})) |
5 | 1, 4 | syl5ibcom 244 |
. . 3
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} → ⚬ :({𝑍} × {𝑍})⟶{𝑍})) |
6 | | fdm 6602 |
. . . . . . 7
⊢ ( ⚬
:(𝐵 × 𝐵)⟶𝐵 → dom ⚬ = (𝐵 × 𝐵)) |
7 | 6 | eqcomd 2744 |
. . . . . 6
⊢ ( ⚬
:(𝐵 × 𝐵)⟶𝐵 → (𝐵 × 𝐵) = dom ⚬ ) |
8 | 7 | adantr 481 |
. . . . 5
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 × 𝐵) = dom ⚬ ) |
9 | | fdm 6602 |
. . . . . 6
⊢ ( ⚬
:({𝑍} × {𝑍})⟶{𝑍} → dom ⚬ = ({𝑍} × {𝑍})) |
10 | 9 | eqeq2d 2749 |
. . . . 5
⊢ ( ⚬
:({𝑍} × {𝑍})⟶{𝑍} → ((𝐵 × 𝐵) = dom ⚬ ↔ (𝐵 × 𝐵) = ({𝑍} × {𝑍}))) |
11 | 8, 10 | syl5ibcom 244 |
. . . 4
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ( ⚬ :({𝑍} × {𝑍})⟶{𝑍} → (𝐵 × 𝐵) = ({𝑍} × {𝑍}))) |
12 | | xpid11 5835 |
. . . 4
⊢ ((𝐵 × 𝐵) = ({𝑍} × {𝑍}) ↔ 𝐵 = {𝑍}) |
13 | 11, 12 | syl6ib 250 |
. . 3
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ( ⚬ :({𝑍} × {𝑍})⟶{𝑍} → 𝐵 = {𝑍})) |
14 | 5, 13 | impbid 211 |
. 2
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ⚬ :({𝑍} × {𝑍})⟶{𝑍})) |
15 | | simpr 485 |
. . . 4
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑍 ∈ 𝐵) |
16 | | xpsng 7004 |
. . . 4
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ({𝑍} × {𝑍}) = {〈𝑍, 𝑍〉}) |
17 | 15, 16 | sylancom 588 |
. . 3
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ({𝑍} × {𝑍}) = {〈𝑍, 𝑍〉}) |
18 | 17 | feq2d 6579 |
. 2
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ( ⚬ :({𝑍} × {𝑍})⟶{𝑍} ↔ ⚬ :{〈𝑍, 𝑍〉}⟶{𝑍})) |
19 | | opex 5378 |
. . . 4
⊢
〈𝑍, 𝑍〉 ∈ V |
20 | | fsng 7002 |
. . . 4
⊢
((〈𝑍, 𝑍〉 ∈ V ∧ 𝑍 ∈ 𝐵) → ( ⚬ :{〈𝑍, 𝑍〉}⟶{𝑍} ↔ ⚬ =
{〈〈𝑍, 𝑍〉, 𝑍〉})) |
21 | 19, 20 | mpan 687 |
. . 3
⊢ (𝑍 ∈ 𝐵 → ( ⚬ :{〈𝑍, 𝑍〉}⟶{𝑍} ↔ ⚬ =
{〈〈𝑍, 𝑍〉, 𝑍〉})) |
22 | 21 | adantl 482 |
. 2
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → ( ⚬ :{〈𝑍, 𝑍〉}⟶{𝑍} ↔ ⚬ =
{〈〈𝑍, 𝑍〉, 𝑍〉})) |
23 | 14, 18, 22 | 3bitrd 305 |
1
⊢ (( ⚬
:(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ⚬ =
{〈〈𝑍, 𝑍〉, 𝑍〉})) |