Metamath Proof Explorer

Theorem fin23lem30

Description: Lemma for fin23 . The residual is disjoint from the common set. (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 fin23lem30 ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ )

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 7 biimpi ⊢ ( 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) → ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) )
9 simpr ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → Fun 𝑡 )
10 5 funmpt2 ⊢ Fun 𝑅
11 funco ⊢ ( ( Fun 𝑡 ∧ Fun 𝑅 ) → Fun ( 𝑡 ∘ 𝑅 ) )
12 9 10 11 sylancl ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → Fun ( 𝑡 ∘ 𝑅 ) )
13 elunirn ⊢ ( Fun ( 𝑡 ∘ 𝑅 ) → ( 𝑎 ∈ ∪ ran ( 𝑡 ∘ 𝑅 ) ↔ ∃ 𝑏 ∈ dom ( 𝑡 ∘ 𝑅 ) 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) ) )
14 12 13 syl ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( 𝑎 ∈ ∪ ran ( 𝑡 ∘ 𝑅 ) ↔ ∃ 𝑏 ∈ dom ( 𝑡 ∘ 𝑅 ) 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) ) )
15 dmcoss ⊢ dom ( 𝑡 ∘ 𝑅 ) ⊆ dom 𝑅
16 15 sseli ⊢ ( 𝑏 ∈ dom ( 𝑡 ∘ 𝑅 ) → 𝑏 ∈ dom 𝑅 )
17 fvco ⊢ ( ( Fun 𝑅 ∧ 𝑏 ∈ dom 𝑅 ) → ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) = ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
18 10 17 mpan ⊢ ( 𝑏 ∈ dom 𝑅 → ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) = ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
19 18 adantl ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) = ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
20 19 eleq2d ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) ↔ 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
21 incom ⊢ ( ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∩ ∩ ran 𝑈 ) = ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
22 difss ⊢ ( ω ∖ 𝑃 ) ⊆ ω
23 ominf ⊢ ¬ ω ∈ Fin
24 3 ssrab3 ⊢ 𝑃 ⊆ ω
25 undif ⊢ ( 𝑃 ⊆ ω ↔ ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) = ω )
26 24 25 mpbi ⊢ ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) = ω
27 unfi ⊢ ( ( 𝑃 ∈ Fin ∧ ( ω ∖ 𝑃 ) ∈ Fin ) → ( 𝑃 ∪ ( ω ∖ 𝑃 ) ) ∈ Fin )
28 26 27 eqeltrrid ⊢ ( ( 𝑃 ∈ Fin ∧ ( ω ∖ 𝑃 ) ∈ Fin ) → ω ∈ Fin )
29 28 ex ⊢ ( 𝑃 ∈ Fin → ( ( ω ∖ 𝑃 ) ∈ Fin → ω ∈ Fin ) )
30 23 29 mtoi ⊢ ( 𝑃 ∈ Fin → ¬ ( ω ∖ 𝑃 ) ∈ Fin )
31 30 ad2antrr ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ¬ ( ω ∖ 𝑃 ) ∈ Fin )
32 5 fin23lem22 ⊢ ( ( ( ω ∖ 𝑃 ) ⊆ ω ∧ ¬ ( ω ∖ 𝑃 ) ∈ Fin ) → 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) )
33 22 31 32 sylancr ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) )
34 f1of ⊢ ( 𝑅 : ω –1-1-onto→ ( ω ∖ 𝑃 ) → 𝑅 : ω ⟶ ( ω ∖ 𝑃 ) )
35 33 34 syl ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → 𝑅 : ω ⟶ ( ω ∖ 𝑃 ) )
36 simpr ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → 𝑏 ∈ dom 𝑅 )
37 35 fdmd ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → dom 𝑅 = ω )
38 36 37 eleqtrd ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → 𝑏 ∈ ω )
39 35 38 ffvelrnd ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( 𝑅 ‘ 𝑏 ) ∈ ( ω ∖ 𝑃 ) )
40 39 eldifbd ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ¬ ( 𝑅 ‘ 𝑏 ) ∈ 𝑃 )
41 3 eleq2i ⊢ ( ( 𝑅 ‘ 𝑏 ) ∈ 𝑃 ↔ ( 𝑅 ‘ 𝑏 ) ∈ { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) } )
42 40 41 sylnib ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ¬ ( 𝑅 ‘ 𝑏 ) ∈ { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) } )
43 39 eldifad ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( 𝑅 ‘ 𝑏 ) ∈ ω )
44 fveq2 ⊢ ( 𝑣 = ( 𝑅 ‘ 𝑏 ) → ( 𝑡 ‘ 𝑣 ) = ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
45 44 sseq2d ⊢ ( 𝑣 = ( 𝑅 ‘ 𝑏 ) → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) ↔ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
46 45 elrab3 ⊢ ( ( 𝑅 ‘ 𝑏 ) ∈ ω → ( ( 𝑅 ‘ 𝑏 ) ∈ { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) } ↔ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
47 43 46 syl ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( ( 𝑅 ‘ 𝑏 ) ∈ { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) } ↔ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
48 42 47 mtbid ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ¬ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) )
49 1 fin23lem20 ⊢ ( ( 𝑅 ‘ 𝑏 ) ∈ ω → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ∅ ) )
50 43 49 syl ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ∅ ) )
51 orel1 ⊢ ( ¬ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) → ( ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ∅ ) → ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ∅ ) )
52 48 50 51 sylc ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ∅ )
53 21 52 syl5eq ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∩ ∩ ran 𝑈 ) = ∅ )
54 disj ⊢ ( ( ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ∩ ∩ ran 𝑈 ) = ∅ ↔ ∀ 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ¬ 𝑎 ∈ ∩ ran 𝑈 )
55 53 54 sylib ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ∀ 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ¬ 𝑎 ∈ ∩ ran 𝑈 )
56 rsp ⊢ ( ∀ 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) ¬ 𝑎 ∈ ∩ ran 𝑈 → ( 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
57 55 56 syl ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( 𝑎 ∈ ( 𝑡 ‘ ( 𝑅 ‘ 𝑏 ) ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
58 20 57 sylbid ⊢ ( ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) ∧ 𝑏 ∈ dom 𝑅 ) → ( 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
59 58 ex ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( 𝑏 ∈ dom 𝑅 → ( 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) ) )
60 16 59 syl5 ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( 𝑏 ∈ dom ( 𝑡 ∘ 𝑅 ) → ( 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) ) )
61 60 rexlimdv ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( ∃ 𝑏 ∈ dom ( 𝑡 ∘ 𝑅 ) 𝑎 ∈ ( ( 𝑡 ∘ 𝑅 ) ‘ 𝑏 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
62 14 61 sylbid ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( 𝑎 ∈ ∪ ran ( 𝑡 ∘ 𝑅 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
63 62 ralrimiv ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ∀ 𝑎 ∈ ∪ ran ( 𝑡 ∘ 𝑅 ) ¬ 𝑎 ∈ ∩ ran 𝑈 )
64 disj ⊢ ( ( ∪ ran ( 𝑡 ∘ 𝑅 ) ∩ ∩ ran 𝑈 ) = ∅ ↔ ∀ 𝑎 ∈ ∪ ran ( 𝑡 ∘ 𝑅 ) ¬ 𝑎 ∈ ∩ ran 𝑈 )
65 63 64 sylibr ⊢ ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( ∪ ran ( 𝑡 ∘ 𝑅 ) ∩ ∩ ran 𝑈 ) = ∅ )
66 rneq ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ran 𝑍 = ran ( 𝑡 ∘ 𝑅 ) )
67 66 unieqd ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ∪ ran 𝑍 = ∪ ran ( 𝑡 ∘ 𝑅 ) )
68 67 ineq1d ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ( ∪ ran ( 𝑡 ∘ 𝑅 ) ∩ ∩ ran 𝑈 ) )
69 68 eqeq1d ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ( ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ↔ ( ∪ ran ( 𝑡 ∘ 𝑅 ) ∩ ∩ ran 𝑈 ) = ∅ ) )
70 65 69 syl5ibr ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ( ( 𝑃 ∈ Fin ∧ Fun 𝑡 ) → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) )
71 70 expd ⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ( 𝑃 ∈ Fin → ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) ) )
72 71 impcom ⊢ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) → ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) )
73 rneq ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ran 𝑍 = ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
74 73 unieqd ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ∪ ran 𝑍 = ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
75 74 ineq1d ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ( ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ∩ ∩ ran 𝑈 ) )
76 rncoss ⊢ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
77 76 unissi ⊢ ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
78 disj ⊢ ( ( ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∩ ∩ ran 𝑈 ) = ∅ ↔ ∀ 𝑎 ∈ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ¬ 𝑎 ∈ ∩ ran 𝑈 )
79 eluniab ⊢ ( 𝑎 ∈ ∪ { 𝑏 ∣ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) } ↔ ∃ 𝑏 ( 𝑎 ∈ 𝑏 ∧ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) )
80 eleq2 ⊢ ( 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → ( 𝑎 ∈ 𝑏 ↔ 𝑎 ∈ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) )
81 eldifn ⊢ ( 𝑎 ∈ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → ¬ 𝑎 ∈ ∩ ran 𝑈 )
82 80 81 syl6bi ⊢ ( 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → ( 𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
83 82 rexlimivw ⊢ ( ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → ( 𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
84 83 impcom ⊢ ( ( 𝑎 ∈ 𝑏 ∧ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) → ¬ 𝑎 ∈ ∩ ran 𝑈 )
85 84 exlimiv ⊢ ( ∃ 𝑏 ( 𝑎 ∈ 𝑏 ∧ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) → ¬ 𝑎 ∈ ∩ ran 𝑈 )
86 79 85 sylbi ⊢ ( 𝑎 ∈ ∪ { 𝑏 ∣ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) } → ¬ 𝑎 ∈ ∩ ran 𝑈 )
87 eqid ⊢ ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
88 87 rnmpt ⊢ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = { 𝑏 ∣ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) }
89 88 unieqi ⊢ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = ∪ { 𝑏 ∣ ∃ 𝑧 ∈ 𝑃 𝑏 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) }
90 86 89 eleq2s ⊢ ( 𝑎 ∈ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) → ¬ 𝑎 ∈ ∩ ran 𝑈 )
91 78 90 mprgbir ⊢ ( ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∩ ∩ ran 𝑈 ) = ∅
92 ssdisj ⊢ ( ( ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∧ ( ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∩ ∩ ran 𝑈 ) = ∅ ) → ( ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ∩ ∩ ran 𝑈 ) = ∅ )
93 77 91 92 mp2an ⊢ ( ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ∩ ∩ ran 𝑈 ) = ∅
94 75 93 syl6eq ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ )
95 94 a1d ⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) )
96 95 adantl ⊢ ( ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) → ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) )
97 72 96 jaoi ⊢ ( ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) → ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ) )
98 6 8 97 mp2b ⊢ ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ )