Metamath Proof Explorer

Theorem dmtposss

Description: The domain of tpos F is a subset. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion dmtposss ⊢ dom ⁡ tpos F ⊆ V × V ∪ ∅

Proof

Step Hyp Ref Expression
1 df-tpos ⊢ tpos F = F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
2 1 dmeqi ⊢ dom ⁡ tpos F = dom ⁡ F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
3 dmcoss ⊢ dom ⁡ F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
4 eqid ⊢ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 = x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
5 4 dmmptss ⊢ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ dom ⁡ F -1 ∪ ∅
6 relcnv ⊢ Rel ⁡ dom ⁡ F -1
7 df-rel ⊢ Rel ⁡ dom ⁡ F -1 ↔ dom ⁡ F -1 ⊆ V × V
8 6 7 mpbi ⊢ dom ⁡ F -1 ⊆ V × V
9 unss1 ⊢ dom ⁡ F -1 ⊆ V × V → dom ⁡ F -1 ∪ ∅ ⊆ V × V ∪ ∅
10 8 9 ax-mp ⊢ dom ⁡ F -1 ∪ ∅ ⊆ V × V ∪ ∅
11 5 10 sstri ⊢ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ V × V ∪ ∅
12 3 11 sstri ⊢ dom ⁡ F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ V × V ∪ ∅
13 2 12 eqsstri ⊢ dom ⁡ tpos F ⊆ V × V ∪ ∅