Proof of Theorem relrelss
| Step | Hyp | Ref
| Expression |
| 1 | | df-rel 5692 |
. . 3
⊢ (Rel dom
𝐴 ↔ dom 𝐴 ⊆ (V ×
V)) |
| 2 | 1 | anbi2i 623 |
. 2
⊢ ((Rel
𝐴 ∧ Rel dom 𝐴) ↔ (Rel 𝐴 ∧ dom 𝐴 ⊆ (V × V))) |
| 3 | | relssdmrn 6288 |
. . . 4
⊢ (Rel
𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) |
| 4 | | ssv 4008 |
. . . . 5
⊢ ran 𝐴 ⊆ V |
| 5 | | xpss12 5700 |
. . . . 5
⊢ ((dom
𝐴 ⊆ (V × V)
∧ ran 𝐴 ⊆ V)
→ (dom 𝐴 × ran
𝐴) ⊆ ((V × V)
× V)) |
| 6 | 4, 5 | mpan2 691 |
. . . 4
⊢ (dom
𝐴 ⊆ (V × V)
→ (dom 𝐴 × ran
𝐴) ⊆ ((V × V)
× V)) |
| 7 | 3, 6 | sylan9ss 3997 |
. . 3
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ (V × V)) →
𝐴 ⊆ ((V × V)
× V)) |
| 8 | | xpss 5701 |
. . . . . 6
⊢ ((V
× V) × V) ⊆ (V × V) |
| 9 | | sstr 3992 |
. . . . . 6
⊢ ((𝐴 ⊆ ((V × V) ×
V) ∧ ((V × V) × V) ⊆ (V × V)) → 𝐴 ⊆ (V ×
V)) |
| 10 | 8, 9 | mpan2 691 |
. . . . 5
⊢ (𝐴 ⊆ ((V × V) ×
V) → 𝐴 ⊆ (V
× V)) |
| 11 | | df-rel 5692 |
. . . . 5
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
| 12 | 10, 11 | sylibr 234 |
. . . 4
⊢ (𝐴 ⊆ ((V × V) ×
V) → Rel 𝐴) |
| 13 | | dmss 5913 |
. . . . 5
⊢ (𝐴 ⊆ ((V × V) ×
V) → dom 𝐴 ⊆ dom
((V × V) × V)) |
| 14 | | vn0 4345 |
. . . . . 6
⊢ V ≠
∅ |
| 15 | | dmxp 5939 |
. . . . . 6
⊢ (V ≠
∅ → dom ((V × V) × V) = (V × V)) |
| 16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢ dom ((V
× V) × V) = (V × V) |
| 17 | 13, 16 | sseqtrdi 4024 |
. . . 4
⊢ (𝐴 ⊆ ((V × V) ×
V) → dom 𝐴 ⊆ (V
× V)) |
| 18 | 12, 17 | jca 511 |
. . 3
⊢ (𝐴 ⊆ ((V × V) ×
V) → (Rel 𝐴 ∧ dom
𝐴 ⊆ (V ×
V))) |
| 19 | 7, 18 | impbii 209 |
. 2
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ (V × V)) ↔
𝐴 ⊆ ((V × V)
× V)) |
| 20 | 2, 19 | bitri 275 |
1
⊢ ((Rel
𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) ×
V)) |