Theorem brtpos0

Description: The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows us to eliminate sethood hypotheses on A , B in brtpos . (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	brtpos0	⊢ ( 𝐴 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		brtpos2	⊢ ( 𝐴 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐴 ↔ ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) ) )
2		ssun2	⊢ { ∅ } ⊆ ( ◡ dom 𝐹 ∪ { ∅ } )
3		0ex	⊢ ∅ ∈ V
4	3	snid	⊢ ∅ ∈ { ∅ }
5	2 4	sselii	⊢ ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } )
6	5	biantrur	⊢ ( ∪ ◡ { ∅ } 𝐹 𝐴 ↔ ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) )
7		cnvsn0	⊢ ◡ { ∅ } = ∅
8	7	unieqi	⊢ ∪ ◡ { ∅ } = ∪ ∅
9		uni0	⊢ ∪ ∅ = ∅
10	8 9	eqtri	⊢ ∪ ◡ { ∅ } = ∅
11	10	breq1i	⊢ ( ∪ ◡ { ∅ } 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 )
12	6 11	bitr3i	⊢ ( ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) ↔ ∅ 𝐹 𝐴 )
13	1 12	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 ) )