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 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 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝐴 } 𝐹 𝐵 ) ) )