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

Metamath Proof Explorer

Theorem fin23lem28

Description: Lemma for fin23 . The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
fin23lem17.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
fin23lem.b ⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
fin23lem.c ⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
fin23lem.d ⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
fin23lem.e ⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
Assertion fin23lem28 ( 𝑡 : ω –1-1→ V → 𝑍 : ω –1-1→ V )

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2 fin23lem17.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3 fin23lem.b ⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
4 fin23lem.c ⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
5 fin23lem.d ⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
6 fin23lem.e ⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
7 eqif ⊢ ( 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ↔ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) )
8 6 7 mpbi ⊢ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) )
9 difss ⊢ ( ω ∖ 𝑃 ) ⊆ ω
10 ominf ⊢ ¬ ω ∈ Fin
11 3 ssrab3 ⊢ 𝑃 ⊆ ω
12 undif ⊢ ( 𝑃 ⊆ ω ↔ ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) = ω )
13 11 12 mpbi ⊢ ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) = ω
14 unfi ⊢ ( ( 𝑃 ∈ Fin ∧ ( ω ∖ 𝑃 ) ∈ Fin ) → ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) ∈ Fin )
15 13 14 eqeltrrid ⊢ ( ( 𝑃 ∈ Fin ∧ ( ω ∖ 𝑃 ) ∈ Fin ) → ω ∈ Fin )
16 15 ex ⊢ ( 𝑃 ∈ Fin → ( ( ω ∖ 𝑃 ) ∈ Fin → ω ∈ Fin ) )
17 10 16 mtoi ⊢ ( 𝑃 ∈ Fin → ¬ ( ω ∖ 𝑃 ) ∈ Fin )
18 5 fin23lem22 ⊢ ( ( ( ω ∖ 𝑃 ) ⊆ ω ∧ ¬ ( ω ∖ 𝑃 ) ∈ Fin ) → 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) )
19 9 17 18 sylancr ⊢ ( 𝑃 ∈ Fin → 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) )
20 19 adantl ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝑃 ∈ Fin ) → 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) )
21 f1of1 ⊢ ( 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) → 𝑅 : ω –1-1→ ( ω ∖ 𝑃 ) )
22 f1ss ⊢ ( ( 𝑅 : ω –1-1→ ( ω ∖ 𝑃 ) ∧ ( ω ∖ 𝑃 ) ⊆ ω ) → 𝑅 : ω –1-1→ ω )
23 9 22 mpan2 ⊢ ( 𝑅 : ω –1-1→ ( ω ∖ 𝑃 ) → 𝑅 : ω –1-1→ ω )
24 20 21 23 3syl ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝑃 ∈ Fin ) → 𝑅 : ω –1-1→ ω )
25 f1co ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝑅 : ω –1-1→ ω ) → ( 𝑡 ∘ 𝑅 ) : ω –1-1→ V )
26 24 25 syldan ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝑃 ∈ Fin ) → ( 𝑡 ∘ 𝑅 ) : ω –1-1→ V )
27 f1eq1 ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ( 𝑍 : ω –1-1→ V ↔ ( 𝑡 ∘ 𝑅 ) : ω –1-1→ V ) )
28 26 27 syl5ibrcom ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝑃 ∈ Fin ) → ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → 𝑍 : ω –1-1→ V ) )
29 28 impr ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ) → 𝑍 : ω –1-1→ V )
30 fvex ⊢ ( 𝑡 ‘ 𝑧 ) ∈ V
31 30 difexi ⊢ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ∈ V
32 31 rgenw ⊢ ∀ 𝑧 ∈ 𝑃 ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ∈ V
33 eqid ⊢ ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
34 33 fmpt ⊢ ( ∀ 𝑧 ∈ 𝑃 ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ∈ V ↔ ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 ⟶ V )
35 32 34 mpbi ⊢ ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 ⟶ V
36 35 a1i ⊢ ( 𝑡 : ω –1-1→ V → ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 ⟶ V )
37 fveq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑡 ‘ 𝑧 ) = ( 𝑡 ‘ 𝑎 ) )
38 37 difeq1d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) )
39 fvex ⊢ ( 𝑡 ‘ 𝑎 ) ∈ V
40 39 difexi ⊢ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) ∈ V
41 38 33 40 fvmpt ⊢ ( 𝑎 ∈ 𝑃 → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) )
42 41 ad2antrl ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) )
43 fveq2 ⊢ ( 𝑧 = 𝑏 → ( 𝑡 ‘ 𝑧 ) = ( 𝑡 ‘ 𝑏 ) )
44 43 difeq1d ⊢ ( 𝑧 = 𝑏 → ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) )
45 fvex ⊢ ( 𝑡 ‘ 𝑏 ) ∈ V
46 45 difexi ⊢ ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ∈ V
47 44 33 46 fvmpt ⊢ ( 𝑏 ∈ 𝑃 → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) )
48 47 ad2antll ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) )
49 42 48 eqeq12d ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) ↔ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ) )
50 uneq2 ⊢ ( ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) → ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) ) = ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ) )
51 fveq2 ⊢ ( 𝑣 = 𝑎 → ( 𝑡 ‘ 𝑣 ) = ( 𝑡 ‘ 𝑎 ) )
52 51 sseq2d ⊢ ( 𝑣 = 𝑎 → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) ↔ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑎 ) ) )
53 52 3 elrab2 ⊢ ( 𝑎 ∈ 𝑃 ↔ ( 𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑎 ) ) )
54 53 simprbi ⊢ ( 𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑎 ) )
55 54 ad2antrl ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑎 ) )
56 undif ⊢ ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑎 ) ↔ ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑡 ‘ 𝑎 ) )
57 55 56 sylib ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑡 ‘ 𝑎 ) )
58 fveq2 ⊢ ( 𝑣 = 𝑏 → ( 𝑡 ‘ 𝑣 ) = ( 𝑡 ‘ 𝑏 ) )
59 58 sseq2d ⊢ ( 𝑣 = 𝑏 → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) ↔ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑏 ) ) )
60 59 3 elrab2 ⊢ ( 𝑏 ∈ 𝑃 ↔ ( 𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑏 ) ) )
61 60 simprbi ⊢ ( 𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑏 ) )
62 61 ad2antll ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑏 ) )
63 undif ⊢ ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑏 ) ↔ ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑡 ‘ 𝑏 ) )
64 62 63 sylib ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑡 ‘ 𝑏 ) )
65 57 64 eqeq12d ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) ) = ( ∩ ran 𝑈 ∪ ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) ) ↔ ( 𝑡 ‘ 𝑎 ) = ( 𝑡 ‘ 𝑏 ) ) )
66 50 65 imbitrid ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) → ( 𝑡 ‘ 𝑎 ) = ( 𝑡 ‘ 𝑏 ) ) )
67 11 sseli ⊢ ( 𝑎 ∈ 𝑃 → 𝑎 ∈ ω )
68 11 sseli ⊢ ( 𝑏 ∈ 𝑃 → 𝑏 ∈ ω )
69 67 68 anim12i ⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) )
70 f1fveq ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( 𝑡 ‘ 𝑎 ) = ( 𝑡 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
71 69 70 sylan2 ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝑡 ‘ 𝑎 ) = ( 𝑡 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
72 66 71 sylibd ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝑡 ‘ 𝑎 ) ∖ ∩ ran 𝑈 ) = ( ( 𝑡 ‘ 𝑏 ) ∖ ∩ ran 𝑈 ) → 𝑎 = 𝑏 ) )
73 49 72 sylbid ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
74 73 ralrimivva ⊢ ( 𝑡 : ω –1-1→ V → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
75 dff13 ⊢ ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 –1-1→ V ↔ ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 ⟶ V ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑎 ) = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
76 36 74 75 sylanbrc ⊢ ( 𝑡 : ω –1-1→ V → ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 –1-1→ V )
77 4 fin23lem22 ⊢ ( ( 𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin ) → 𝑄 : ω –1-1-onto→ 𝑃 )
78 f1of1 ⊢ ( 𝑄 : ω –1-1-onto→ 𝑃 → 𝑄 : ω –1-1→ 𝑃 )
79 77 78 syl ⊢ ( ( 𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin ) → 𝑄 : ω –1-1→ 𝑃 )
80 11 79 mpan ⊢ ( ¬ 𝑃 ∈ Fin → 𝑄 : ω –1-1→ 𝑃 )
81 f1co ⊢ ( ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) : 𝑃 –1-1→ V ∧ 𝑄 : ω –1-1→ 𝑃 ) → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) : ω –1-1→ V )
82 76 80 81 syl2an ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ¬ 𝑃 ∈ Fin ) → ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) : ω –1-1→ V )
83 f1eq1 ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ( 𝑍 : ω –1-1→ V ↔ ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) : ω –1-1→ V ) )
84 82 83 syl5ibrcom ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ¬ 𝑃 ∈ Fin ) → ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → 𝑍 : ω –1-1→ V ) )
85 84 impr ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) → 𝑍 : ω –1-1→ V )
86 29 85 jaodan ⊢ ( ( 𝑡 : ω –1-1→ V ∧ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) ) → 𝑍 : ω –1-1→ V )
87 8 86 mpan2 ⊢ ( 𝑡 : ω –1-1→ V → 𝑍 : ω –1-1→ V )