Theorem tpostpos 6243

Description: Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.)

Assertion

Ref	Expression
tpostpos	⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))

Proof of Theorem tpostpos

Dummy variables 𝑥 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reltpos 6229	. 2 ⊢ Rel tpos tpos 𝐹
2		inss2 3348	. . 3 ⊢ (𝐹 ∩ (((V × V) ∪ {∅}) × V)) ⊆ (((V × V) ∪ {∅}) × V)
3		relxp 4720	. . 3 ⊢ Rel (((V × V) ∪ {∅}) × V)
4		relss 4698	. . 3 ⊢ ((𝐹 ∩ (((V × V) ∪ {∅}) × V)) ⊆ (((V × V) ∪ {∅}) × V) → (Rel (((V × V) ∪ {∅}) × V) → Rel (𝐹 ∩ (((V × V) ∪ {∅}) × V))))
5	2, 3, 4	mp2 16	. 2 ⊢ Rel (𝐹 ∩ (((V × V) ∪ {∅}) × V))
6		relcnv 4989	. . . . . . . . 9 ⊢ Rel ◡dom tpos 𝐹
7		df-rel 4618	. . . . . . . . 9 ⊢ (Rel ◡dom tpos 𝐹 ↔ ◡dom tpos 𝐹 ⊆ (V × V))
8	6, 7	mpbi 144	. . . . . . . 8 ⊢ ◡dom tpos 𝐹 ⊆ (V × V)
9		simpl 108	. . . . . . . 8 ⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ ◡dom tpos 𝐹)
10	8, 9	sselid 3145	. . . . . . 7 ⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ (V × V))
11		simpr 109	. . . . . . 7 ⊢ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) → 𝑤 ∈ (V × V))
12		elvv 4673	. . . . . . . . 9 ⊢ (𝑤 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩)
13		eleq1 2233	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹))
14		vex 2733	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
15		vex 2733	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
16	14, 15	opelcnv 4793	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹)
17	13, 16	bitrdi 195	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹))
18		sneq 3594	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → {𝑤} = {⟨𝑥, 𝑦⟩})
19	18	cnveqd 4787	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ◡{𝑤} = ◡{⟨𝑥, 𝑦⟩})
20	19	unieqd 3807	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪ ◡{𝑤} = ∪ ◡{⟨𝑥, 𝑦⟩})
21		opswapg 5097	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ∪ ◡{⟨𝑥, 𝑦⟩} = ⟨𝑦, 𝑥⟩)
22	14, 15, 21	mp2an 424	. . . . . . . . . . . . . . 15 ⊢ ∪ ◡{⟨𝑥, 𝑦⟩} = ⟨𝑦, 𝑥⟩
23	20, 22	eqtrdi 2219	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪ ◡{𝑤} = ⟨𝑦, 𝑥⟩)
24	23	breq1d 3999	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧))
25	17, 24	anbi12d 470	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧)))
26	15, 14	opex 4214	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑦, 𝑥⟩ ∈ V
27		vex 2733	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
28	26, 27	breldm 4815	. . . . . . . . . . . . . 14 ⊢ (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 → ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹)
29	28	pm4.71ri 390	. . . . . . . . . . . . 13 ⊢ (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧))
30		brtposg 6233	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ V ∧ 𝑥 ∈ V ∧ 𝑧 ∈ V) → (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧))
31	15, 14, 27, 30	mp3an 1332	. . . . . . . . . . . . 13 ⊢ (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)
32	29, 31	bitr3i 185	. . . . . . . . . . . 12 ⊢ ((⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)
33	25, 32	bitrdi 195	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧))
34		breq1 3992	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧))
35	33, 34	bitr4d 190	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧))
36	35	exlimivv 1889	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧))
37	12, 36	sylbi 120	. . . . . . . 8 ⊢ (𝑤 ∈ (V × V) → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧))
38		iba 298	. . . . . . . 8 ⊢ (𝑤 ∈ (V × V) → (𝑤𝐹𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))))
39	37, 38	bitrd 187	. . . . . . 7 ⊢ (𝑤 ∈ (V × V) → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))))
40	10, 11, 39	pm5.21nii 699	. . . . . 6 ⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))
41		elsni 3601	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ {∅} → 𝑤 = ∅)
42	41	sneqd 3596	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {∅} → {𝑤} = {∅})
43	42	cnveqd 4787	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ◡{∅})
44		cnvsn0 5079	. . . . . . . . . . . . . 14 ⊢ ◡{∅} = ∅
45	43, 44	eqtrdi 2219	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ∅)
46	45	unieqd 3807	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∪ ∅)
47		uni0 3823	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
48	46, 47	eqtrdi 2219	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∅)
49	48	breq1d 3999	. . . . . . . . . 10 ⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅tpos 𝐹𝑧))
50		brtpos0 6231	. . . . . . . . . . 11 ⊢ (𝑧 ∈ V → (∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧))
51	27, 50	ax-mp 5	. . . . . . . . . 10 ⊢ (∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧)
52	49, 51	bitrdi 195	. . . . . . . . 9 ⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅𝐹𝑧))
53	41	breq1d 3999	. . . . . . . . 9 ⊢ (𝑤 ∈ {∅} → (𝑤𝐹𝑧 ↔ ∅𝐹𝑧))
54	52, 53	bitr4d 190	. . . . . . . 8 ⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ 𝑤𝐹𝑧))
55	54	pm5.32i 451	. . . . . . 7 ⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧))
56		ancom 264	. . . . . . 7 ⊢ ((𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))
57	55, 56	bitri 183	. . . . . 6 ⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))
58	40, 57	orbi12i 759	. . . . 5 ⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})))
59		andir 814	. . . . 5 ⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)))
60		andi 813	. . . . 5 ⊢ ((𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})))
61	58, 59, 60	3bitr4i 211	. . . 4 ⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})))
62		elun 3268	. . . . 5 ⊢ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ↔ (𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}))
63	62	anbi1i 455	. . . 4 ⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))
64		brxp 4642	. . . . . . 7 ⊢ (𝑤(((V × V) ∪ {∅}) × V)𝑧 ↔ (𝑤 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 ∈ V))
65	27, 64	mpbiran2 936	. . . . . 6 ⊢ (𝑤(((V × V) ∪ {∅}) × V)𝑧 ↔ 𝑤 ∈ ((V × V) ∪ {∅}))
66		elun 3268	. . . . . 6 ⊢ (𝑤 ∈ ((V × V) ∪ {∅}) ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))
67	65, 66	bitri 183	. . . . 5 ⊢ (𝑤(((V × V) ∪ {∅}) × V)𝑧 ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))
68	67	anbi2i 454	. . . 4 ⊢ ((𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) × V)𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})))
69	61, 63, 68	3bitr4i 211	. . 3 ⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) × V)𝑧))
70		brtpos2 6230	. . . 4 ⊢ (𝑧 ∈ V → (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)))
71	27, 70	ax-mp 5	. . 3 ⊢ (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))
72		brin 4041	. . 3 ⊢ (𝑤(𝐹 ∩ (((V × V) ∪ {∅}) × V))𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) × V)𝑧))
73	69, 71, 72	3bitr4i 211	. 2 ⊢ (𝑤tpos tpos 𝐹𝑧 ↔ 𝑤(𝐹 ∩ (((V × V) ∪ {∅}) × V))𝑧)
74	1, 5, 73	eqbrriv 4706	1 ⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))

Syntax hints:   ∧ wa 103   ↔ wb 104   ∨ wo 703   = wceq 1348  ∃wex 1485   ∈ wcel 2141  Vcvv 2730   ∪ cun 3119   ∩ cin 3120   ⊆ wss 3121  ∅c0 3414  {csn 3583  ⟨cop 3586  ∪ cuni 3796   class class class wbr 3989   × cxp 4609  ^◡ccnv 4610  dom cdm 4611  Rel wrel 4616  tpos ctpos 6223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-fv 5206  df-tpos 6224

This theorem is referenced by:  tpostpos2  6244