Metamath Proof Explorer


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 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 ) )