Metamath Proof Explorer

Theorem wrd2f1tovbij

Description: There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018)

Ref Expression
Assertion wrd2f1tovbij ⊢ V ∈ Y ∧ P ∈ V → ∃ f f : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X

Proof

Step Hyp Ref Expression
1 wrdexg ⊢ V ∈ Y → Word V ∈ V
2 1 adantr ⊢ V ∈ Y ∧ P ∈ V → Word V ∈ V
3 rabexg ⊢ Word V ∈ V → t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ∈ V
4 mptexg ⊢ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ∈ V → x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 ∈ V
5 2 3 4 3syl ⊢ V ∈ Y ∧ P ∈ V → x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 ∈ V
6 fveqeq2 ⊢ w = u → w = 2 ↔ u = 2
7 fveq1 ⊢ w = u → w ⁡ 0 = u ⁡ 0
8 7 eqeq1d ⊢ w = u → w ⁡ 0 = P ↔ u ⁡ 0 = P
9 fveq1 ⊢ w = u → w ⁡ 1 = u ⁡ 1
10 7 9 preq12d ⊢ w = u → w ⁡ 0 w ⁡ 1 = u ⁡ 0 u ⁡ 1
11 10 eleq1d ⊢ w = u → w ⁡ 0 w ⁡ 1 ∈ X ↔ u ⁡ 0 u ⁡ 1 ∈ X
12 6 8 11 3anbi123d ⊢ w = u → w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ↔ u = 2 ∧ u ⁡ 0 = P ∧ u ⁡ 0 u ⁡ 1 ∈ X
13 12 cbvrabv ⊢ w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X = u ∈ Word V | u = 2 ∧ u ⁡ 0 = P ∧ u ⁡ 0 u ⁡ 1 ∈ X
14 preq2 ⊢ n = p → P n = P p
15 14 eleq1d ⊢ n = p → P n ∈ X ↔ P p ∈ X
16 15 cbvrabv ⊢ n ∈ V | P n ∈ X = p ∈ V | P p ∈ X
17 fveqeq2 ⊢ t = w → t = 2 ↔ w = 2
18 fveq1 ⊢ t = w → t ⁡ 0 = w ⁡ 0
19 18 eqeq1d ⊢ t = w → t ⁡ 0 = P ↔ w ⁡ 0 = P
20 fveq1 ⊢ t = w → t ⁡ 1 = w ⁡ 1
21 18 20 preq12d ⊢ t = w → t ⁡ 0 t ⁡ 1 = w ⁡ 0 w ⁡ 1
22 21 eleq1d ⊢ t = w → t ⁡ 0 t ⁡ 1 ∈ X ↔ w ⁡ 0 w ⁡ 1 ∈ X
23 17 19 22 3anbi123d ⊢ t = w → t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ↔ w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X
24 23 cbvrabv ⊢ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X = w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X
25 24 mpteq1i ⊢ x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 = x ∈ w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟼ x ⁡ 1
26 13 16 25 wwlktovf1o ⊢ P ∈ V → x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X
27 26 adantl ⊢ V ∈ Y ∧ P ∈ V → x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X
28 f1oeq1 ⊢ f = x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 → f : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X ↔ x ∈ t ∈ Word V | t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X ⟼ x ⁡ 1 : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X
29 5 27 28 spcedv ⊢ V ∈ Y ∧ P ∈ V → ∃ f f : w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ⟶ 1-1 onto n ∈ V | P n ∈ X