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 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ 𝑦 , 𝑥𝐹 𝑧 } )