Proof of Theorem ustneism
Step | Hyp | Ref
| Expression |
1 | | snnzg 4774 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → {𝐴} ≠ ∅) |
2 | 1 | adantl 480 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → {𝐴} ≠ ∅) |
3 | | xpco 6291 |
. . 3
⊢ ({𝐴} ≠ ∅ → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) = ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴}))) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) = ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴}))) |
5 | | cnvxp 6159 |
. . . . 5
⊢ ◡({𝐴} × (𝑉 “ {𝐴})) = ((𝑉 “ {𝐴}) × {𝐴}) |
6 | | ressn 6287 |
. . . . . . 7
⊢ (𝑉 ↾ {𝐴}) = ({𝐴} × (𝑉 “ {𝐴})) |
7 | 6 | cnveqi 5872 |
. . . . . 6
⊢ ◡(𝑉 ↾ {𝐴}) = ◡({𝐴} × (𝑉 “ {𝐴})) |
8 | | resss 6002 |
. . . . . . 7
⊢ (𝑉 ↾ {𝐴}) ⊆ 𝑉 |
9 | | cnvss 5870 |
. . . . . . 7
⊢ ((𝑉 ↾ {𝐴}) ⊆ 𝑉 → ◡(𝑉 ↾ {𝐴}) ⊆ ◡𝑉) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ◡(𝑉 ↾ {𝐴}) ⊆ ◡𝑉 |
11 | 7, 10 | eqsstrri 4015 |
. . . . 5
⊢ ◡({𝐴} × (𝑉 “ {𝐴})) ⊆ ◡𝑉 |
12 | 5, 11 | eqsstrri 4015 |
. . . 4
⊢ ((𝑉 “ {𝐴}) × {𝐴}) ⊆ ◡𝑉 |
13 | | coss2 5854 |
. . . 4
⊢ (((𝑉 “ {𝐴}) × {𝐴}) ⊆ ◡𝑉 → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉)) |
14 | 12, 13 | mp1i 13 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉)) |
15 | 6, 8 | eqsstrri 4015 |
. . . 4
⊢ ({𝐴} × (𝑉 “ {𝐴})) ⊆ 𝑉 |
16 | | coss1 5853 |
. . . 4
⊢ (({𝐴} × (𝑉 “ {𝐴})) ⊆ 𝑉 → (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉) ⊆ (𝑉 ∘ ◡𝑉)) |
17 | 15, 16 | mp1i 13 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉) ⊆ (𝑉 ∘ ◡𝑉)) |
18 | 14, 17 | sstrd 3990 |
. 2
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (𝑉 ∘ ◡𝑉)) |
19 | 4, 18 | eqsstrrd 4019 |
1
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴})) ⊆ (𝑉 ∘ ◡𝑉)) |