Theorem dmtposss

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

	Ref	Expression
Assertion	dmtposss	⊢ dom tpos 𝐹 ⊆ ( ( V × V ) ∪ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
2	1	dmeqi	⊢ dom tpos 𝐹 = dom ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
3		dmcoss	⊢ dom ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
4		eqid	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
5	4	dmmptss	⊢ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( ◡ dom 𝐹 ∪ { ∅ } )
6		relcnv	⊢ Rel ◡ dom 𝐹
7		df-rel	⊢ ( Rel ◡ dom 𝐹 ↔ ◡ dom 𝐹 ⊆ ( V × V ) )
8	6 7	mpbi	⊢ ◡ dom 𝐹 ⊆ ( V × V )
9		unss1	⊢ ( ◡ dom 𝐹 ⊆ ( V × V ) → ( ◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ( V × V ) ∪ { ∅ } ) )
10	8 9	ax-mp	⊢ ( ◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ( V × V ) ∪ { ∅ } )
11	5 10	sstri	⊢ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( ( V × V ) ∪ { ∅ } )
12	3 11	sstri	⊢ dom ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ ( ( V × V ) ∪ { ∅ } )
13	2 12	eqsstri	⊢ dom tpos 𝐹 ⊆ ( ( V × V ) ∪ { ∅ } )