This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmtpos

Description: The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dmtpos ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 )

Proof

Step Hyp Ref Expression
1 0nelxp ⊢ ¬ ∅ ∈ ( V × V )
2 ssel ⊢ ( dom 𝐹 ⊆ ( V × V ) → ( ∅ ∈ dom 𝐹 → ∅ ∈ ( V × V ) ) )
3 1 2 mtoi ⊢ ( dom 𝐹 ⊆ ( V × V ) → ¬ ∅ ∈ dom 𝐹 )
4 df-rel ⊢ ( Rel dom 𝐹 ↔ dom 𝐹 ⊆ ( V × V ) )
5 reldmtpos ⊢ ( Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹 )
6 3 4 5 3imtr4i ⊢ ( Rel dom 𝐹 → Rel dom tpos 𝐹 )
7 relcnv ⊢ Rel ◡ dom 𝐹
8 6 7 jctir ⊢ ( Rel dom 𝐹 → ( Rel dom tpos 𝐹 ∧ Rel ◡ dom 𝐹 ) )
9 vex ⊢ 𝑧 ∈ V
10 brtpos ⊢ ( 𝑧 ∈ V → ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
11 9 10 mp1i ⊢ ( Rel dom 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
12 11 exbidv ⊢ ( Rel dom 𝐹 → ( ∃ 𝑧 ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
13 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
14 13 eldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom tpos 𝐹 ↔ ∃ 𝑧 ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 )
15 vex ⊢ 𝑥 ∈ V
16 vex ⊢ 𝑦 ∈ V
17 15 16 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ dom 𝐹 )
18 opex ⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
19 18 eldm ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom 𝐹 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 )
20 17 19 bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom 𝐹 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 )
21 12 14 20 3bitr4g ⊢ ( Rel dom 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom tpos 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom 𝐹 ) )
22 21 eqrelrdv2 ⊢ ( ( ( Rel dom tpos 𝐹 ∧ Rel ◡ dom 𝐹 ) ∧ Rel dom 𝐹 ) → dom tpos 𝐹 = ◡ dom 𝐹 )
23 8 22 mpancom ⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 )