fin23lem30 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin23lem30		Structured version Visualization version GIF version

Theorem fin23lem30 10341

Description: Lemma for fin23 10388. 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 4531	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	2	biimpi 219	. 2 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
4		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → Fun 𝑡)
5		fin23lem.d	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
6	5	funmpt2 6579	. . . . . . . . . . 11 ⊢ Fun 𝑅
7		funco 6580	. . . . . . . . . . 11 ⊢ ((Fun 𝑡 ∧ Fun 𝑅) → Fun (𝑡 ∘ 𝑅))
8	4, 6, 7	sylancl 598	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → Fun (𝑡 ∘ 𝑅))
9		elunirn 7254	. . . . . . . . . 10 ⊢ (Fun (𝑡 ∘ 𝑅) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
10	8, 9	syl 18	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
11		dmcoss 5967	. . . . . . . . . . . 12 ⊢ dom (𝑡 ∘ 𝑅) ⊆ dom 𝑅
12	11	sseli 3934	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom (𝑡 ∘ 𝑅) → 𝑏 ∈ dom 𝑅)
13		fvco 6983	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑅 ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
14	6, 13	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ dom 𝑅 → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
15	14	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
16	15	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) ↔ 𝑎 ∈ (𝑡‘(𝑅‘𝑏))))
17		incom 4162	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏)))
18		difss 4090	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∖ 𝑃) ⊆ ω
19		ominf 9231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ¬ ω ∈ Fin
20		fin23lem.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
21	20	ssrab3 4037	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑃 ⊆ ω
22		undif 4445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
23	21, 22	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
24		unfi 9162	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
25	23, 24	eqeltrrid 2870	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → ω ∈ Fin)
26	25	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ Fin → ((ω ∖ 𝑃) ∈ Fin → ω ∈ Fin))
27	19, 26	mtoi 202	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ Fin → ¬ (ω ∖ 𝑃) ∈ Fin)
28	27	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (ω ∖ 𝑃) ∈ Fin)
29	5	fin23lem22 10326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
30	18, 28, 29	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
31		f1of 6824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω⟶(ω ∖ 𝑃))
32	30, 31	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω⟶(ω ∖ 𝑃))
33		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ dom 𝑅)
34	32	fdmd 6720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → dom 𝑅 = ω)
35	33, 34	eleqtrd 2867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ ω)
36	32, 35	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ (ω ∖ 𝑃))
37	36	eldifbd 3919	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ 𝑃)
38	20	eleq2i 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅‘𝑏) ∈ 𝑃 ↔ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
39	37, 38	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
40	36	eldifad 3918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ ω)
41		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑅‘𝑏) → (𝑡‘𝑣) = (𝑡‘(𝑅‘𝑏)))
42	41	sseq2d 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = (𝑅‘𝑏) → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
43	42	elrab3 3653	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅‘𝑏) ∈ ω → ((𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
44	40, 43	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
45	39, 44	mtbid 327	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)))
46		fin23lem.a	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑈 = seq_ω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)
47	46	fin23lem20 10336	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑏) ∈ ω → (∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
48	40, 47	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
49		orel1 902	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) → ((∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏)) ∨ (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅) → (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅))
50	45, 48, 49	sylc 66	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏))) = ∅)
51	17, 50	eqtrid 2812	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅)
52		disj 4410	. . . . . . . . . . . . . . 15 ⊢ (((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
53	51, 52	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
54		rsp 3255	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈 → (𝑎 ∈ (𝑡‘(𝑅‘𝑏)) → ¬ 𝑎 ∈ ∩ ran 𝑈))
55	53, 54	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ (𝑡‘(𝑅‘𝑏)) → ¬ 𝑎 ∈ ∩ ran 𝑈))
56	16, 55	sylbid 243	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈))
57	56	ex 418	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑏 ∈ dom 𝑅 → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈)))
58	12, 57	syl5 35	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑏 ∈ dom (𝑡 ∘ 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈)))
59	58	rexlimdv 3166	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈))
60	10, 59	sylbid 243	. . . . . . . 8 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) → ¬ 𝑎 ∈ ∩ ran 𝑈))
61	60	ralrimiv 3158	. . . . . . 7 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
62		disj 4410	. . . . . . 7 ⊢ ((∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
63	61, 62	sylibr 237	. . . . . 6 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅)
64		rneq 5928	. . . . . . . . 9 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ran 𝑍 = ran (𝑡 ∘ 𝑅))
65	64	unieqd 4887	. . . . . . . 8 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran 𝑍 = ∪ ran (𝑡 ∘ 𝑅))
66	65	ineq1d 4172	. . . . . . 7 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈))
67	66	eqeq1d 2767	. . . . . 6 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ((∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅ ↔ (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅))
68	63, 67	imbitrrid 249	. . . . 5 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
69	68	expd 421	. . . 4 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (𝑃 ∈ Fin → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)))
70	69	impcom 413	. . 3 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
71		rneq 5928	. . . . . . . 8 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
72	71	unieqd 4887	. . . . . . 7 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ∪ ran 𝑍 = ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
73	72	ineq1d 4172	. . . . . 6 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈))
74		rncoss 5969	. . . . . . . 8 ⊢ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
75	74	unissi 4883	. . . . . . 7 ⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
76		disj 4410	. . . . . . . 8 ⊢ ((∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ¬ 𝑎 ∈ ∩ ran 𝑈)
77		eluniab 4888	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)} ↔ ∃𝑏(𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
78		eleq2 2854	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
79		eldifn 4086	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → ¬ 𝑎 ∈ ∩ ran 𝑈)
80	78, 79	biimtrdi 256	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈))
81	80	rexlimivw 3164	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈))
82	81	impcom 413	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
83	82	exlimiv 1963	. . . . . . . . . 10 ⊢ (∃𝑏(𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
84	77, 83	sylbi 220	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)} → ¬ 𝑎 ∈ ∩ ran 𝑈)
85		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
86	85	rnmpt 5949	. . . . . . . . . 10 ⊢ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
87	86	unieqi 4886	. . . . . . . . 9 ⊢ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
88	84, 87	eleq2s 2883	. . . . . . . 8 ⊢ (𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
89	76, 88	mprgbir 3088	. . . . . . 7 ⊢ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅
90		ssdisj 4420	. . . . . . 7 ⊢ ((∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∧ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅) → (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈) = ∅)
91	75, 89, 90	mp2an 705	. . . . . 6 ⊢ (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈) = ∅
92	73, 91	eqtrdi 2816	. . . . 5 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)
93	92	a1d 26	. . . 4 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
94	93	adantl 487	. . 3 ⊢ ((¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
95	70, 94	jaoi 871	. 2 ⊢ (((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))) → (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅))
96	1, 3, 95	mp2b 10	1 ⊢ (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∃wex 1812 ∈ wcel 2146 {cab 2743 ∀wral 3081 ∃wrex 3091 {crab 3418 Vcvv 3457 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4286 ifcif 4489 𝒫 cpw 4564 ∪ cuni 4874 ∩ cint 4914 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ran crn 5664 ∘ ccom 5667 suc csuc 6366 Fun wfun 6534 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 ℩crio 7375 (class class class)co 7419 ∈ cmpo 7421 ωcom 7868 seq_ωcseqom 8440 ↑_m cmap 8830 ≈ cen 8946 Fincfn 8949

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-seqom 8441 df-1o 8459 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-card 9941

This theorem is used by: fin23lem31 10342

W3C validator