Proof of Theorem ustneism
| Step | Hyp | Ref
| Expression |
| 1 | | snnzg 4774 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → {𝐴} ≠ ∅) |
| 2 | 1 | adantl 481 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → {𝐴} ≠ ∅) |
| 3 | | xpco 6309 |
. . 3
⊢ ({𝐴} ≠ ∅ → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) = ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴}))) |
| 4 | 2, 3 | syl 17 |
. 2
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) = ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴}))) |
| 5 | | cnvxp 6177 |
. . . . 5
⊢ ◡({𝐴} × (𝑉 “ {𝐴})) = ((𝑉 “ {𝐴}) × {𝐴}) |
| 6 | | ressn 6305 |
. . . . . . 7
⊢ (𝑉 ↾ {𝐴}) = ({𝐴} × (𝑉 “ {𝐴})) |
| 7 | 6 | cnveqi 5885 |
. . . . . 6
⊢ ◡(𝑉 ↾ {𝐴}) = ◡({𝐴} × (𝑉 “ {𝐴})) |
| 8 | | resss 6019 |
. . . . . . 7
⊢ (𝑉 ↾ {𝐴}) ⊆ 𝑉 |
| 9 | | cnvss 5883 |
. . . . . . 7
⊢ ((𝑉 ↾ {𝐴}) ⊆ 𝑉 → ◡(𝑉 ↾ {𝐴}) ⊆ ◡𝑉) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ◡(𝑉 ↾ {𝐴}) ⊆ ◡𝑉 |
| 11 | 7, 10 | eqsstrri 4031 |
. . . . 5
⊢ ◡({𝐴} × (𝑉 “ {𝐴})) ⊆ ◡𝑉 |
| 12 | 5, 11 | eqsstrri 4031 |
. . . 4
⊢ ((𝑉 “ {𝐴}) × {𝐴}) ⊆ ◡𝑉 |
| 13 | | coss2 5867 |
. . . 4
⊢ (((𝑉 “ {𝐴}) × {𝐴}) ⊆ ◡𝑉 → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉)) |
| 14 | 12, 13 | mp1i 13 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉)) |
| 15 | 6, 8 | eqsstrri 4031 |
. . . 4
⊢ ({𝐴} × (𝑉 “ {𝐴})) ⊆ 𝑉 |
| 16 | | coss1 5866 |
. . . 4
⊢ (({𝐴} × (𝑉 “ {𝐴})) ⊆ 𝑉 → (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉) ⊆ (𝑉 ∘ ◡𝑉)) |
| 17 | 15, 16 | mp1i 13 |
. . 3
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ◡𝑉) ⊆ (𝑉 ∘ ◡𝑉)) |
| 18 | 14, 17 | sstrd 3994 |
. 2
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → (({𝐴} × (𝑉 “ {𝐴})) ∘ ((𝑉 “ {𝐴}) × {𝐴})) ⊆ (𝑉 ∘ ◡𝑉)) |
| 19 | 4, 18 | eqsstrrd 4019 |
1
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴})) ⊆ (𝑉 ∘ ◡𝑉)) |