Metamath Proof Explorer


Theorem brtpos2

Description: Value of the transposition at a 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 syl5bb ( ( 𝐴 ∈ 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 𝐹 ∪ { ∅ } ) ∧ { 𝐴 } 𝐹 𝐵 ) ) )