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