Theorem tpostpos

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

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

Proof

Step	Hyp	Ref	Expression
1		reltpos	⊢ Rel tpos tpos 𝐹
2		relinxp	⊢ Rel ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
3		relcnv	⊢ Rel ◡ dom tpos 𝐹
4		df-rel	⊢ ( Rel ◡ dom tpos 𝐹 ↔ ◡ dom tpos 𝐹 ⊆ ( V × V ) )
5	3 4	mpbi	⊢ ◡ dom tpos 𝐹 ⊆ ( V × V )
6		simpl	⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) → 𝑤 ∈ ◡ dom tpos 𝐹 )
7	5 6	sselid	⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) → 𝑤 ∈ ( V × V ) )
8		simpr	⊢ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) → 𝑤 ∈ ( V × V ) )
9		elvv	⊢ ( 𝑤 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
10		eleq1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom tpos 𝐹 ) )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13	11 12	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 )
14	10 13	bitrdi	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ) )
15		sneq	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑤 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
16	15	cnveqd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ◡ { 𝑤 } = ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
17	16	unieqd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ ◡ { 𝑤 } = ∪ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
18		opswap	⊢ ∪ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } = ⟨ 𝑦 , 𝑥 ⟩
19	17 18	eqtrdi	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ ◡ { 𝑤 } = ⟨ 𝑦 , 𝑥 ⟩ )
20	19	breq1d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) )
21	14 20	anbi12d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) ) )
22		opex	⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
23		vex	⊢ 𝑧 ∈ V
24	22 23	breldm	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 → ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 )
25	24	pm4.71ri	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) )
26		brtpos	⊢ ( 𝑧 ∈ V → ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
27	26	elv	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 )
28	25 27	bitr3i	⊢ ( ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 )
29	21 28	bitrdi	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
30		breq1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
31	29 30	bitr4d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
32	31	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
33	9 32	sylbi	⊢ ( 𝑤 ∈ ( V × V ) → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
34		iba	⊢ ( 𝑤 ∈ ( V × V ) → ( 𝑤 𝐹 𝑧 ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ) )
35	33 34	bitrd	⊢ ( 𝑤 ∈ ( V × V ) → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ) )
36	7 8 35	pm5.21nii	⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) )
37		elsni	⊢ ( 𝑤 ∈ { ∅ } → 𝑤 = ∅ )
38	37	sneqd	⊢ ( 𝑤 ∈ { ∅ } → { 𝑤 } = { ∅ } )
39	38	cnveqd	⊢ ( 𝑤 ∈ { ∅ } → ◡ { 𝑤 } = ◡ { ∅ } )
40		cnvsn0	⊢ ◡ { ∅ } = ∅
41	39 40	eqtrdi	⊢ ( 𝑤 ∈ { ∅ } → ◡ { 𝑤 } = ∅ )
42	41	unieqd	⊢ ( 𝑤 ∈ { ∅ } → ∪ ◡ { 𝑤 } = ∪ ∅ )
43		uni0	⊢ ∪ ∅ = ∅
44	42 43	eqtrdi	⊢ ( 𝑤 ∈ { ∅ } → ∪ ◡ { 𝑤 } = ∅ )
45	44	breq1d	⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ∅ tpos 𝐹 𝑧 ) )
46		brtpos0	⊢ ( 𝑧 ∈ V → ( ∅ tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
47	46	elv	⊢ ( ∅ tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 )
48	45 47	bitrdi	⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
49	37	breq1d	⊢ ( 𝑤 ∈ { ∅ } → ( 𝑤 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
50	48 49	bitr4d	⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ 𝑤 𝐹 𝑧 ) )
51	50	pm5.32i	⊢ ( ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 ∈ { ∅ } ∧ 𝑤 𝐹 𝑧 ) )
52	51	biancomi	⊢ ( ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) )
53	36 52	orbi12i	⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ∨ ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) ↔ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ∨ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) ) )
54		andir	⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ∨ ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) )
55		andi	⊢ ( ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) ↔ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ∨ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) ) )
56	53 54 55	3bitr4i	⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) )
57		elun	⊢ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ↔ ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) )
58	57	anbi1i	⊢ ( ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) )
59		brxp	⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ ( 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 ∈ V ) )
60	23 59	mpbiran2	⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) )
61		elun	⊢ ( 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) ↔ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) )
62	60 61	bitri	⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) )
63	62	anbi2i	⊢ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) )
64	56 58 63	3bitr4i	⊢ ( ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) )
65		brtpos2	⊢ ( 𝑧 ∈ V → ( 𝑤 tpos tpos 𝐹 𝑧 ↔ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) )
66	65	elv	⊢ ( 𝑤 tpos tpos 𝐹 𝑧 ↔ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) )
67		brin	⊢ ( 𝑤 ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) 𝑧 ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) )
68	64 66 67	3bitr4i	⊢ ( 𝑤 tpos tpos 𝐹 𝑧 ↔ 𝑤 ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) 𝑧 )
69	1 2 68	eqbrriv	⊢ tpos tpos 𝐹 = ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )