Theorem dftpos3 5818

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

Assertion

Ref	Expression
dftpos3	⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ⟨y, x⟩𝐹z})

Distinct variable group:   x,y,z,𝐹

Proof of Theorem dftpos3

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		relcnv 4646	. . . . . . . . . 10 ⊢ Rel ◡dom 𝐹
2		dmtpos 5812	. . . . . . . . . . 11 ⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹)
3	2	releqd 4367	. . . . . . . . . 10 ⊢ (Rel dom 𝐹 → (Rel dom tpos 𝐹 ↔ Rel ◡dom 𝐹))
4	1, 3	mpbiri 157	. . . . . . . . 9 ⊢ (Rel dom 𝐹 → Rel dom tpos 𝐹)
5		reltpos 5806	. . . . . . . . 9 ⊢ Rel tpos 𝐹
6	4, 5	jctil 295	. . . . . . . 8 ⊢ (Rel dom 𝐹 → (Rel tpos 𝐹 ∧ Rel dom tpos 𝐹))
7		relrelss 4787	. . . . . . . 8 ⊢ ((Rel tpos 𝐹 ∧ Rel dom tpos 𝐹) ↔ tpos 𝐹 ⊆ ((V × V) × V))
8	6, 7	sylib 127	. . . . . . 7 ⊢ (Rel dom 𝐹 → tpos 𝐹 ⊆ ((V × V) × V))
9	8	sseld 2938	. . . . . 6 ⊢ (Rel dom 𝐹 → (w ∈ tpos 𝐹 → w ∈ ((V × V) × V)))
10		elvvv 4346	. . . . . 6 ⊢ (w ∈ ((V × V) × V) ↔ ∃x∃y∃z w = ⟨⟨x, y⟩, z⟩)
11	9, 10	syl6ib 150	. . . . 5 ⊢ (Rel dom 𝐹 → (w ∈ tpos 𝐹 → ∃x∃y∃z w = ⟨⟨x, y⟩, z⟩))
12	11	pm4.71rd 374	. . . 4 ⊢ (Rel dom 𝐹 → (w ∈ tpos 𝐹 ↔ (∃x∃y∃z w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹)))
13		19.41vvv 1781	. . . . 5 ⊢ (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹) ↔ (∃x∃y∃z w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹))
14		eleq1 2097	. . . . . . . 8 ⊢ (w = ⟨⟨x, y⟩, z⟩ → (w ∈ tpos 𝐹 ↔ ⟨⟨x, y⟩, z⟩ ∈ tpos 𝐹))
15		df-br 3756	. . . . . . . . 9 ⊢ (⟨x, y⟩tpos 𝐹z ↔ ⟨⟨x, y⟩, z⟩ ∈ tpos 𝐹)
16		vex 2554	. . . . . . . . . 10 ⊢ x ∈ V
17		vex 2554	. . . . . . . . . 10 ⊢ y ∈ V
18		vex 2554	. . . . . . . . . 10 ⊢ z ∈ V
19		brtposg 5810	. . . . . . . . . 10 ⊢ ((x ∈ V ∧ y ∈ V ∧ z ∈ V) → (⟨x, y⟩tpos 𝐹z ↔ ⟨y, x⟩𝐹z))
20	16, 17, 18, 19	mp3an 1231	. . . . . . . . 9 ⊢ (⟨x, y⟩tpos 𝐹z ↔ ⟨y, x⟩𝐹z)
21	15, 20	bitr3i 175	. . . . . . . 8 ⊢ (⟨⟨x, y⟩, z⟩ ∈ tpos 𝐹 ↔ ⟨y, x⟩𝐹z)
22	14, 21	syl6bb 185	. . . . . . 7 ⊢ (w = ⟨⟨x, y⟩, z⟩ → (w ∈ tpos 𝐹 ↔ ⟨y, x⟩𝐹z))
23	22	pm5.32i 427	. . . . . 6 ⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹) ↔ (w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z))
24	23	3exbii 1495	. . . . 5 ⊢ (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹) ↔ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z))
25	13, 24	bitr3i 175	. . . 4 ⊢ ((∃x∃y∃z w = ⟨⟨x, y⟩, z⟩ ∧ w ∈ tpos 𝐹) ↔ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z))
26	12, 25	syl6bb 185	. . 3 ⊢ (Rel dom 𝐹 → (w ∈ tpos 𝐹 ↔ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z)))
27	26	abbi2dv 2153	. 2 ⊢ (Rel dom 𝐹 → tpos 𝐹 = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z)})
28		df-oprab 5459	. 2 ⊢ {⟨⟨x, y⟩, z⟩ ∣ ⟨y, x⟩𝐹z} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ ⟨y, x⟩𝐹z)}
29	27, 28	syl6eqr 2087	1 ⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ⟨y, x⟩𝐹z})

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  Vcvv 2551   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755   × cxp 4286  ^◡ccnv 4287  dom cdm 4288  Rel wrel 4293  {coprab 5456  tpos ctpos 5800

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853  df-oprab 5459  df-tpos 5801

This theorem is referenced by:  tposoprab  5836