Theorem brtpos2

Description: Value of the transposition at an ordered pair <. A , B >. . (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	brtpos2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reltpos	⊢ Rel tpos 𝐹
2	1	brrelex1i	⊢ ( 𝐴 tpos 𝐹 𝐵 → 𝐴 ∈ V )
3	2	a1i	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 tpos 𝐹 𝐵 → 𝐴 ∈ V ) )
4		elex	⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → 𝐴 ∈ V )
5	4	adantr	⊢ ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) → 𝐴 ∈ V )
6	5	a1i	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) → 𝐴 ∈ V ) )
7		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
8	7	breqi	⊢ ( 𝐴 tpos 𝐹 𝐵 ↔ 𝐴 ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) 𝐵 )
9		brcog	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) 𝐵 ↔ ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ) )
10	8 9	bitrid	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 tpos 𝐹 𝐵 ↔ ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ) )
11		funmpt	⊢ Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
12		funbrfv2b	⊢ ( Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) → ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ) )
13	11 12	ax-mp	⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) )
14		snex	⊢ { 𝑥 } ∈ V
15	14	cnvex	⊢ ◡ { 𝑥 } ∈ V
16	15	uniex	⊢ ∪ ◡ { 𝑥 } ∈ V
17		eqid	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
18	16 17	dmmpti	⊢ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( ◡ dom 𝐹 ∪ { ∅ } )
19	18	eleq2i	⊢ ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↔ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
20		eqcom	⊢ ( ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ↔ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) )
21	19 20	anbi12i	⊢ ( ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ) )
22		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
23	22	cnveqd	⊢ ( 𝑥 = 𝐴 → ◡ { 𝑥 } = ◡ { 𝐴 } )
24	23	unieqd	⊢ ( 𝑥 = 𝐴 → ∪ ◡ { 𝑥 } = ∪ ◡ { 𝐴 } )
25		snex	⊢ { 𝐴 } ∈ V
26	25	cnvex	⊢ ◡ { 𝐴 } ∈ V
27	26	uniex	⊢ ∪ ◡ { 𝐴 } ∈ V
28	24 17 27	fvmpt	⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = ∪ ◡ { 𝐴 } )
29	28	eqeq2d	⊢ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) → ( 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ↔ 𝑦 = ∪ ◡ { 𝐴 } ) )
30	29	pm5.32i	⊢ ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) )
31	21 30	bitri	⊢ ( ( 𝐴 ∈ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ‘ 𝐴 ) = 𝑦 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) )
32	13 31	bitri	⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 = ∪ ◡ { 𝐴 } ) )
33	32	biancomi	⊢ ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) )
34	33	anbi1i	⊢ ( ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 𝐹 𝐵 ) )
35		anass	⊢ ( ( ( 𝑦 = ∪ ◡ { 𝐴 } ∧ 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) )
36	34 35	bitri	⊢ ( ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) )
37	36	exbii	⊢ ( ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) )
38		breq1	⊢ ( 𝑦 = ∪ ◡ { 𝐴 } → ( 𝑦 𝐹 𝐵 ↔ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) )
39	38	anbi2d	⊢ ( 𝑦 = ∪ ◡ { 𝐴 } → ( ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) )
40	27 39	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = ∪ ◡ { 𝐴 } ∧ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 𝑦 𝐹 𝐵 ) ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) )
41	37 40	bitri	⊢ ( ∃ 𝑦 ( 𝐴 ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑦 ∧ 𝑦 𝐹 𝐵 ) ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) )
42	10 41	bitrdi	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) )
43	42	expcom	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) ) )
44	3 6 43	pm5.21ndd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 tpos 𝐹 𝐵 ↔ ( 𝐴 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) )