Theorem fin23lem30 10278

Description: Lemma for fin23 10325. The residual is disjoint from the common set. (Contributed by Stefan O'Rear, 2-Nov-2014.)

Hypotheses

Ref	Expression
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

Ref	Expression
fin23lem30	⊢ (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)

Distinct variable groups:   𝑔,𝑖,𝑡,𝑢,𝑣,𝑥,𝑧,𝑎   𝐹,𝑎,𝑡   𝑤,𝑎,𝑥,𝑧,𝑃   𝑣,𝑎,𝑅,𝑖,𝑢   𝑈,𝑎,𝑖,𝑢,𝑣,𝑧   𝑍,𝑎   𝑔,𝑎

Allowed substitution hints:   𝑃(𝑣,𝑢,𝑡,𝑔,𝑖)   𝑄(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,𝑔,𝑖,𝑎)   𝑅(𝑥,𝑧,𝑤,𝑡,𝑔)   𝑈(𝑥,𝑤,𝑡,𝑔)   𝐹(𝑥,𝑧,𝑤,𝑣,𝑢,𝑔,𝑖)   𝑍(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,𝑔,𝑖)

Proof of Theorem fin23lem30

Dummy variable 𝑏 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fin23lem.e	. 2 ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
2		eqif 4527	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	2	biimpi 215	. 2 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
4		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → Fun 𝑡)
5		fin23lem.d	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
6	5	funmpt2 6540	. . . . . . . . . . 11 ⊢ Fun 𝑅
7		funco 6541	. . . . . . . . . . 11 ⊢ ((Fun 𝑡 ∧ Fun 𝑅) → Fun (𝑡 ∘ 𝑅))
8	4, 6, 7	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → Fun (𝑡 ∘ 𝑅))
9		elunirn 7198	. . . . . . . . . 10 ⊢ (Fun (𝑡 ∘ 𝑅) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
11		dmcoss 5926	. . . . . . . . . . . 12 ⊢ dom (𝑡 ∘ 𝑅) ⊆ dom 𝑅
12	11	sseli 3940	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom (𝑡 ∘ 𝑅) → 𝑏 ∈ dom 𝑅)
13		fvco 6939	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑅 ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
14	6, 13	mpan 688	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ dom 𝑅 → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
15	14	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
16	15	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) ↔ 𝑎 ∈ (𝑡‘(𝑅‘𝑏))))
17		incom 4161	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏)))
18		difss 4091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∖ 𝑃) ⊆ ω
19		ominf 9202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ¬ ω ∈ Fin
20		fin23lem.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
21	20	ssrab3 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑃 ⊆ ω
22		undif 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
23	21, 22	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
24		unfi 9116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
25	23, 24	eqeltrrid 2843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → ω ∈ Fin)
26	25	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ Fin → ((ω ∖ 𝑃) ∈ Fin → ω ∈ Fin))
27	19, 26	mtoi 198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ Fin → ¬ (ω ∖ 𝑃) ∈ Fin)
28	27	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (ω ∖ 𝑃) ∈ Fin)
29	5	fin23lem22 10263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
30	18, 28, 29	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
31		f1of 6784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω⟶(ω ∖ 𝑃))
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω⟶(ω ∖ 𝑃))
33		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ dom 𝑅)
34	32	fdmd 6679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → dom 𝑅 = ω)
35	33, 34	eleqtrd 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ ω)
36	32, 35	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ (ω ∖ 𝑃))
37	36	eldifbd 3923	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ 𝑃)
38	20	eleq2i 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅‘𝑏) ∈ 𝑃 ↔ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
39	37, 38	sylnib 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
40	36	eldifad 3922	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ ω)
41		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑅‘𝑏) → (𝑡‘𝑣) = (𝑡‘(𝑅‘𝑏)))
42	41	sseq2d 3976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = (𝑅‘𝑏) → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
43	42	elrab3 3646	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅‘𝑏) ∈ ω → ((𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
44	40, 43	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
45	39, 44	mtbid 323	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)))
46		fin23lem.a	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)
47	46	fin23lem20 10273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑏) ∈ ω → (∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
48	40, 47	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
49		orel1 887	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) → ((∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅) → (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
50	45, 48, 49	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅)
51	17, 50	eqtrid 2788	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅)
52		disj 4407	. . . . . . . . . . . . . . 15 ⊢ (((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
53	51, 52	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
54		rsp 3230	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈 → (𝑎 ∈ (𝑡‘(𝑅‘𝑏)) → ¬ 𝑎 ∈ ∩ ran 𝑈))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ (𝑡‘(𝑅‘𝑏)) → ¬ 𝑎 ∈ ∩ ran 𝑈))
56	16, 55	sylbid 239	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈))
57	56	ex 413	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑏 ∈ dom 𝑅 → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈)))
58	12, 57	syl5 34	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑏 ∈ dom (𝑡 ∘ 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈)))
59	58	rexlimdv 3150	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈))
60	10, 59	sylbid 239	. . . . . . . 8 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) → ¬ 𝑎 ∈ ∩ ran 𝑈))
61	60	ralrimiv 3142	. . . . . . 7 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
62		disj 4407	. . . . . . 7 ⊢ ((∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
63	61, 62	sylibr 233	. . . . . 6 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅)
64		rneq 5891	. . . . . . . . 9 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ran 𝑍 = ran (𝑡 ∘ 𝑅))
65	64	unieqd 4879	. . . . . . . 8 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran 𝑍 = ∪ ran (𝑡 ∘ 𝑅))
66	65	ineq1d 4171	. . . . . . 7 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈))
67	66	eqeq1d 2738	. . . . . 6 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ((∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅ ↔ (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅))
68	63, 67	syl5ibr 245	. . . . 5 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
69	68	expd 416	. . . 4 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (𝑃 ∈ Fin → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)))
70	69	impcom 408	. . 3 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
71		rneq 5891	. . . . . . . 8 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
72	71	unieqd 4879	. . . . . . 7 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ∪ ran 𝑍 = ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
73	72	ineq1d 4171	. . . . . 6 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈))
74		rncoss 5927	. . . . . . . 8 ⊢ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
75	74	unissi 4874	. . . . . . 7 ⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
76		disj 4407	. . . . . . . 8 ⊢ ((∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ¬ 𝑎 ∈ ∩ ran 𝑈)
77		eluniab 4880	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)} ↔ ∃𝑏(𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
78		eleq2 2826	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
79		eldifn 4087	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → ¬ 𝑎 ∈ ∩ ran 𝑈)
80	78, 79	syl6bi 252	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈))
81	80	rexlimivw 3148	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈))
82	81	impcom 408	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
83	82	exlimiv 1933	. . . . . . . . . 10 ⊢ (∃𝑏(𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
84	77, 83	sylbi 216	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)} → ¬ 𝑎 ∈ ∩ ran 𝑈)
85		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
86	85	rnmpt 5910	. . . . . . . . . 10 ⊢ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
87	86	unieqi 4878	. . . . . . . . 9 ⊢ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
88	84, 87	eleq2s 2856	. . . . . . . 8 ⊢ (𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
89	76, 88	mprgbir 3071	. . . . . . 7 ⊢ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅
90		ssdisj 4419	. . . . . . 7 ⊢ ((∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∧ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅) → (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈) = ∅)
91	75, 89, 90	mp2an 690	. . . . . 6 ⊢ (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈) = ∅
92	73, 91	eqtrdi 2792	. . . . 5 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)
93	92	a1d 25	. . . 4 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
94	93	adantl 482	. . 3 ⊢ ((¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
95	70, 94	jaoi 855	. 2 ⊢ (((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
96	1, 3, 95	mp2b 10	1 ⊢ (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  ifcif 4486  𝒫 cpw 4560  ∪ cuni 4865  ∩ cint 4907   class class class wbr 5105   ↦ cmpt 5188  dom cdm 5633  ran crn 5634   ∘ ccom 5637  suc csuc 6319  Fun wfun 6490  ⟶wf 6492  –1-1-onto→wf1o 6495  ‘cfv 6496  ℩crio 7312  (class class class)co 7357   ∈ cmpo 7359  ωcom 7802  seq_ωcseqom 8393   ↑_m cmap 8765   ≈ cen 8880  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-seqom 8394  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9875

This theorem is referenced by:  fin23lem31  10279