Theorem fseqen

Description: A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014)

	Ref	Expression
Assertion	fseqen	⊢ ( ( ( 𝐴 × 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bren	⊢ ( ( 𝐴 × 𝐴 ) ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
2		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐴 )
3		exdistrv	⊢ ( ∃ 𝑓 ∃ 𝑏 ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ↔ ( ∃ 𝑓 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ ∃ 𝑏 𝑏 ∈ 𝐴 ) )
4		omex	⊢ ω ∈ V
5		simpl	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
6		f1ofo	⊢ ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 → 𝑓 : ( 𝐴 × 𝐴 ) –onto→ 𝐴 )
7		forn	⊢ ( 𝑓 : ( 𝐴 × 𝐴 ) –onto→ 𝐴 → ran 𝑓 = 𝐴 )
8	5 6 7	3syl	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ran 𝑓 = 𝐴 )
9		vex	⊢ 𝑓 ∈ V
10	9	rnex	⊢ ran 𝑓 ∈ V
11	8 10	eqeltrrdi	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → 𝐴 ∈ V )
12		xpexg	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ V ) → ( ω × 𝐴 ) ∈ V )
13	4 11 12	sylancr	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ω × 𝐴 ) ∈ V )
14		simpr	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ 𝐴 )
15		eqid	⊢ seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } ) = seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } )
16		eqid	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ⟨ dom 𝑥 , ( ( seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } ) ‘ dom 𝑥 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ⟨ dom 𝑥 , ( ( seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } ) ‘ dom 𝑥 ) ‘ 𝑥 ) ⟩ )
17	11 14 5 15 16	fseqenlem2	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ⟨ dom 𝑥 , ( ( seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } ) ‘ dom 𝑥 ) ‘ 𝑥 ) ⟩ ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) –1-1→ ( ω × 𝐴 ) )
18		f1domg	⊢ ( ( ω × 𝐴 ) ∈ V → ( ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ⟨ dom 𝑥 , ( ( seqω ( ( 𝑘 ∈ V , 𝑔 ∈ V ↦ ( 𝑦 ∈ ( 𝐴 ↑m suc 𝑘 ) ↦ ( ( 𝑔 ‘ ( 𝑦 ↾ 𝑘 ) ) 𝑓 ( 𝑦 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , 𝑏 ⟩ } ) ‘ dom 𝑥 ) ‘ 𝑥 ) ⟩ ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) –1-1→ ( ω × 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ ( ω × 𝐴 ) ) )
19	13 17 18	sylc	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ ( ω × 𝐴 ) )
20		fseqdom	⊢ ( 𝐴 ∈ V → ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
21	11 20	syl	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
22		sbth	⊢ ( ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ ( ω × 𝐴 ) ∧ ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
23	19 21 22	syl2anc	⊢ ( ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
24	23	exlimivv	⊢ ( ∃ 𝑓 ∃ 𝑏 ( 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
25	3 24	sylbir	⊢ ( ( ∃ 𝑓 𝑓 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ∧ ∃ 𝑏 𝑏 ∈ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
26	1 2 25	syl2anb	⊢ ( ( ( 𝐴 × 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )