Theorem tmachlem-uassst

Description: Union of all agreement sets only includes tapes. (Contributed by Ender Ting, 28-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
	tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
	tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
	tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
	tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion	tmachlem-uassst	⊢ ( 𝜑 → ∪ ran 𝐴 ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	⊢ ( 𝜑 → 𝑈 ∈ Fin )
2		tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
3		tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
4		tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
5		tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
6		tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
7	5	rneqd	⊢ ( 𝜑 → ran 𝐴 = ran ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
8	7	unieqd	⊢ ( 𝜑 → ∪ ran 𝐴 = ∪ ran ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
9	1 2 3 4 5 6	tmachlem-extapes	⊢ ( 𝜑 → 𝑇 ∈ V )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → 𝑇 ∈ V )
11		ssrab2	⊢ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇 )
13	10 12	ssexd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
14	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
15		dfiun3g	⊢ ( ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V → ∪ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } = ∪ ran ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
16	14 15	syl	⊢ ( 𝜑 → ∪ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } = ∪ ran ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
17	8 16	eqtr4d	⊢ ( 𝜑 → ∪ ran 𝐴 = ∪ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } )
18	12	iunssd	⊢ ( 𝜑 → ∪ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇 )
19	17 18	eqsstrd	⊢ ( 𝜑 → ∪ ran 𝐴 ⊆ 𝑇 )