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 𝐹 )