This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } )