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 ( ( 𝑉𝑌𝑃𝑉 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } )

Proof

Step Hyp Ref Expression
1 wrdexg ( 𝑉𝑌 → Word 𝑉 ∈ V )
2 1 adantr ( ( 𝑉𝑌𝑃𝑉 ) → Word 𝑉 ∈ V )
3 rabexg ( Word 𝑉 ∈ V → { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ∈ V )
4 mptexg ( { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ∈ V → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) ∈ V )
5 2 3 4 3syl ( ( 𝑉𝑌𝑃𝑉 ) → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) ∈ V )
6 fveqeq2 ( 𝑤 = 𝑢 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑢 ) = 2 ) )
7 fveq1 ( 𝑤 = 𝑢 → ( 𝑤 ‘ 0 ) = ( 𝑢 ‘ 0 ) )
8 7 eqeq1d ( 𝑤 = 𝑢 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑢 ‘ 0 ) = 𝑃 ) )
9 fveq1 ( 𝑤 = 𝑢 → ( 𝑤 ‘ 1 ) = ( 𝑢 ‘ 1 ) )
10 7 9 preq12d ( 𝑤 = 𝑢 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } )
11 10 eleq1d ( 𝑤 = 𝑢 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
12 6 8 11 3anbi123d ( 𝑤 = 𝑢 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
13 12 cbvrabv { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } = { 𝑢 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) }
14 preq2 ( 𝑛 = 𝑝 → { 𝑃 , 𝑛 } = { 𝑃 , 𝑝 } )
15 14 eleq1d ( 𝑛 = 𝑝 → ( { 𝑃 , 𝑛 } ∈ 𝑋 ↔ { 𝑃 , 𝑝 } ∈ 𝑋 ) )
16 15 cbvrabv { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } = { 𝑝𝑉 ∣ { 𝑃 , 𝑝 } ∈ 𝑋 }
17 fveqeq2 ( 𝑡 = 𝑤 → ( ( ♯ ‘ 𝑡 ) = 2 ↔ ( ♯ ‘ 𝑤 ) = 2 ) )
18 fveq1 ( 𝑡 = 𝑤 → ( 𝑡 ‘ 0 ) = ( 𝑤 ‘ 0 ) )
19 18 eqeq1d ( 𝑡 = 𝑤 → ( ( 𝑡 ‘ 0 ) = 𝑃 ↔ ( 𝑤 ‘ 0 ) = 𝑃 ) )
20 fveq1 ( 𝑡 = 𝑤 → ( 𝑡 ‘ 1 ) = ( 𝑤 ‘ 1 ) )
21 18 20 preq12d ( 𝑡 = 𝑤 → { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } = { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } )
22 21 eleq1d ( 𝑡 = 𝑤 → ( { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) )
23 17 19 22 3anbi123d ( 𝑡 = 𝑤 → ( ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ) )
24 23 cbvrabv { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
25 24 mpteq1i ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) = ( 𝑥 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) )
26 13 16 25 wwlktovf1o ( 𝑃𝑉 → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } )
27 26 adantl ( ( 𝑉𝑌𝑃𝑉 ) → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } )
28 f1oeq1 ( 𝑓 = ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) → ( 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ↔ ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ) )
29 5 27 28 spcedv ( ( 𝑉𝑌𝑃𝑉 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } )