Metamath Proof Explorer

Theorem dftpos3

Description: Alternate definition of tpos when F has relational domain. Compare df-cnv . (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dftpos3 ( Rel dom 𝐹 → tpos 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 } )

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ◡ dom 𝐹
2 dmtpos ⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 )
3 2 releqd ⊢ ( Rel dom 𝐹 → ( Rel dom tpos 𝐹 ↔ Rel ◡ dom 𝐹 ) )
4 1 3 mpbiri ⊢ ( Rel dom 𝐹 → Rel dom tpos 𝐹 )
5 reltpos ⊢ Rel tpos 𝐹
6 4 5 jctil ⊢ ( Rel dom 𝐹 → ( Rel tpos 𝐹 ∧ Rel dom tpos 𝐹 ) )
7 relrelss ⊢ ( ( Rel tpos 𝐹 ∧ Rel dom tpos 𝐹 ) ↔ tpos 𝐹 ⊆ ( ( V × V ) × V ) )
8 6 7 sylib ⊢ ( Rel dom 𝐹 → tpos 𝐹 ⊆ ( ( V × V ) × V ) )
9 8 sseld ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ tpos 𝐹 → 𝑤 ∈ ( ( V × V ) × V ) ) )
10 elvvv ⊢ ( 𝑤 ∈ ( ( V × V ) × V ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
11 9 10 syl6ib ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ tpos 𝐹 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
12 11 pm4.71rd ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ tpos 𝐹 ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) ) )
13 19.41vvv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) )
14 eleq1 ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ tpos 𝐹 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ tpos 𝐹 ) )
15 df-br ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ tpos 𝐹 )
16 brtpos ⊢ ( 𝑧 ∈ V → ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
17 16 elv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 )
18 15 17 bitr3i ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 )
19 14 18 bitrdi ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑤 ∈ tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
20 19 pm5.32i ⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) ↔ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
21 20 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
22 13 21 bitr3i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 ∈ tpos 𝐹 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) )
23 12 22 bitrdi ⊢ ( Rel dom 𝐹 → ( 𝑤 ∈ tpos 𝐹 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) ) )
24 23 abbi2dv ⊢ ( Rel dom 𝐹 → tpos 𝐹 = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) } )
25 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 ) }
26 24 25 eqtr4di ⊢ ( Rel dom 𝐹 → tpos 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ 𝑦 , 𝑥 ⟩ 𝐹 𝑧 } )