Metamath Proof Explorer

Theorem tmachlem-agreeprod

Description: Agreement set can be written as infinite product of acceptable values for tape's cells. (Contributed by Ender Ting, 27-Jul-2026)

Ref Expression
Hypotheses tmach.finalph ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-agreeprod ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑎 ) = X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) )

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 fveq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑎 ) )
8 7 reseq2d ⊢ ( 𝑧 = 𝑎 → ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) )
9 id ⊢ ( 𝑧 = 𝑎 → 𝑧 = 𝑎 )
10 9 7 reseq12d ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) ↔ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ) )
12 11 rabbidv ⊢ ( 𝑧 = 𝑎 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } = { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ 𝑇 )
15 1 2 3 4 5 6 tmachlem-extapes ⊢ ( 𝜑 → 𝑇 ∈ V )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑇 ∈ V )
17 ssrab2 ⊢ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ⊆ 𝑇
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ⊆ 𝑇 )
19 16 18 ssexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ∈ V )
20 12 13 14 19 fvmptd4 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑎 ) = { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
21 snfi ⊢ { ( 𝑎 ‘ 𝑖 ) } ∈ Fin
22 21 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → { ( 𝑎 ‘ 𝑖 ) } ∈ Fin )
23 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑈 ∈ Fin )
24 22 23 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ∈ Fin )
25 24 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∀ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ∈ Fin )
26 ixpssmapg ⊢ ( ∀ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ∈ Fin → X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ ( ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↑m 𝐼 ) )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ ( ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↑m 𝐼 ) )
28 ifssun ⊢ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ ( { ( 𝑎 ‘ 𝑖 ) } ∪ 𝑈 )
29 3 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑇 ↔ 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) ) )
30 29 biimpd ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑇 → 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) ) )
31 30 imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) )
32 elmapi ⊢ ( 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝑈 )
33 31 32 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 : 𝐼 ⟶ 𝑈 )
34 33 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑖 ) ∈ 𝑈 )
35 34 snssd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → { ( 𝑎 ‘ 𝑖 ) } ⊆ 𝑈 )
36 ssequn1 ⊢ ( { ( 𝑎 ‘ 𝑖 ) } ⊆ 𝑈 ↔ ( { ( 𝑎 ‘ 𝑖 ) } ∪ 𝑈 ) = 𝑈 )
37 35 36 sylib ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → ( { ( 𝑎 ‘ 𝑖 ) } ∪ 𝑈 ) = 𝑈 )
38 28 37 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ 𝑈 )
39 38 iunssd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ 𝑈 )
40 mapss ⊢ ( ( 𝑈 ∈ Fin ∧ ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ 𝑈 ) → ( ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↑m 𝐼 ) ⊆ ( 𝑈 ↑m 𝐼 ) )
41 1 39 40 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ∪ 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↑m 𝐼 ) ⊆ ( 𝑈 ↑m 𝐼 ) )
42 27 41 sstrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ ( 𝑈 ↑m 𝐼 ) )
43 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
44 42 43 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ⊆ 𝑇 )
45 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) )
46 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
47 45 46 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) )
48 fvex ⊢ ( 𝑦 ‘ 𝑖 ) ∈ V
49 48 elsn ⊢ ( ( 𝑦 ‘ 𝑖 ) ∈ { ( 𝑎 ‘ 𝑖 ) } ↔ ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) )
50 47 49 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ { ( 𝑎 ‘ 𝑖 ) } )
51 45 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) = { ( 𝑎 ‘ 𝑖 ) } )
52 50 51 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) )
53 52 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) )
54 53 a1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) → ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
55 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( 𝒫 𝐼 ∩ Fin ) )
56 55 elin1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ∈ 𝒫 𝐼 )
57 56 elpwid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ⊆ 𝐼 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ⊆ 𝐼 )
59 58 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → 𝑖 ∈ 𝐼 )
60 59 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → 𝑖 ∈ 𝐼 )
61 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) )
62 60 61 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) )
63 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) )
64 63 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) = { ( 𝑎 ‘ 𝑖 ) } )
65 62 64 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ { ( 𝑎 ‘ 𝑖 ) } )
66 65 elsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) )
67 66 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
68 67 a1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) → ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) )
69 54 68 impbid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
70 3 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑇 ↔ 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) ) )
71 70 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑇 → 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑦 ∈ 𝑇 → 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) ) )
73 72 imp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) )
74 elmapi ⊢ ( 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) → 𝑦 : 𝐼 ⟶ 𝑈 )
75 73 74 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 : 𝐼 ⟶ 𝑈 )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → 𝑦 : 𝐼 ⟶ 𝑈 )
77 76 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ 𝑈 )
78 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ 𝑖 ∈ 𝐼 ) → ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) )
79 78 iffalsed ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) = 𝑈 )
80 77 79 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) )
81 80 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) )
82 81 a1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) → ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
83 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) )
84 83 pm2.21d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) ∧ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) → ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
85 84 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) → ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ) )
86 82 85 impbid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) ∧ ¬ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
87 69 86 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) → ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝐼 → ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
88 87 ralbidv2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( ∀ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) )
89 71 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) )
90 elmapfn ⊢ ( 𝑦 ∈ ( 𝑈 ↑m 𝐼 ) → 𝑦 Fn 𝐼 )
91 89 90 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 Fn 𝐼 )
92 91 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 Fn 𝐼 )
93 92 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
94 88 93 bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( ( 𝑦 Fn 𝐼 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ↔ ∀ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
95 vex ⊢ 𝑦 ∈ V
96 95 elixp ⊢ ( 𝑦 ∈ X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) )
97 96 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑦 ∈ X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ) ) )
98 elmapfn ⊢ ( 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) → 𝑎 Fn 𝐼 )
99 31 98 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 Fn 𝐼 )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑎 Fn 𝐼 )
101 fvreseq ⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑎 Fn 𝐼 ) ∧ ( 𝑆 ‘ 𝑎 ) ⊆ 𝐼 ) → ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ↔ ∀ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
102 92 100 58 101 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ↔ ∀ 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) ) )
103 94 97 102 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑦 ∈ X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) ↔ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ) )
104 44 103 eqrrabd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) = { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
105 20 104 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑎 ) = X 𝑖 ∈ 𝐼 if ( 𝑖 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑖 ) } , 𝑈 ) )