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 10333

Description: Lemma for fin23 10380. 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 4568	. . 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 6584	. . . . . . . . . . 11 ⊢ Fun 𝑅
7		funco 6585	. . . . . . . . . . 11 ⊢ ((Fun 𝑡 ∧ Fun 𝑅) → Fun (𝑡 ∘ 𝑅))
8	4, 6, 7	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → Fun (𝑡 ∘ 𝑅))
9		elunirn 7246	. . . . . . . . . 10 ⊢ (Fun (𝑡 ∘ 𝑅) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ↔ ∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏)))
11		dmcoss 5968	. . . . . . . . . . . 12 ⊢ dom (𝑡 ∘ 𝑅) ⊆ dom 𝑅
12	11	sseli 3977	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom (𝑡 ∘ 𝑅) → 𝑏 ∈ dom 𝑅)
13		fvco 6986	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑅 ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
14	6, 13	mpan 688	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ dom 𝑅 → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
15	14	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡 ∘ 𝑅)‘𝑏) = (𝑡‘(𝑅‘𝑏)))
16	15	eleq2d 2819	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) ↔ 𝑎 ∈ (𝑡‘(𝑅‘𝑏))))
17		incom 4200	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = (∩ ran 𝑈 ∩ (𝑡‘(𝑅‘𝑏)))
18		difss 4130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∖ 𝑃) ⊆ ω
19		ominf 9254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ¬ ω ∈ Fin
20		fin23lem.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
21	20	ssrab3 4079	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑃 ⊆ ω
22		undif 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
23	21, 22	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
24		unfi 9168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
25	23, 24	eqeltrrid 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 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 10318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
30	18, 28, 29	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
31		f1of 6830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω⟶(ω ∖ 𝑃))
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑅:ω⟶(ω ∖ 𝑃))
33		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ dom 𝑅)
34	32	fdmd 6725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → dom 𝑅 = ω)
35	33, 34	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → 𝑏 ∈ ω)
36	32, 35	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ (ω ∖ 𝑃))
37	36	eldifbd 3960	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ 𝑃)
38	20	eleq2i 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅‘𝑏) ∈ 𝑃 ↔ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
39	37, 38	sylnib 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ¬ (𝑅‘𝑏) ∈ {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)})
40	36	eldifad 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → (𝑅‘𝑏) ∈ ω)
41		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑅‘𝑏) → (𝑡‘𝑣) = (𝑡‘(𝑅‘𝑏)))
42	41	sseq2d 4013	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = (𝑅‘𝑏) → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘(𝑅‘𝑏))))
43	42	elrab3 3683	. . . . . . . . . . . . . . . . . . 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 10328	. . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅)
52		disj 4446	. . . . . . . . . . . . . . 15 ⊢ (((𝑡‘(𝑅‘𝑏)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
53	51, 52	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Fin ∧ Fun 𝑡) ∧ 𝑏 ∈ dom 𝑅) → ∀𝑎 ∈ (𝑡‘(𝑅‘𝑏)) ¬ 𝑎 ∈ ∩ ran 𝑈)
54		rsp 3244	. . . . . . . . . . . . . 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 3153	. . . . . . . . 9 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∃𝑏 ∈ dom (𝑡 ∘ 𝑅)𝑎 ∈ ((𝑡 ∘ 𝑅)‘𝑏) → ¬ 𝑎 ∈ ∩ ran 𝑈))
60	10, 59	sylbid 239	. . . . . . . 8 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) → ¬ 𝑎 ∈ ∩ ran 𝑈))
61	60	ralrimiv 3145	. . . . . . 7 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
62		disj 4446	. . . . . . 7 ⊢ ((∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑡 ∘ 𝑅) ¬ 𝑎 ∈ ∩ ran 𝑈)
63	61, 62	sylibr 233	. . . . . 6 ⊢ ((𝑃 ∈ Fin ∧ Fun 𝑡) → (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅)
64		rneq 5933	. . . . . . . . 9 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ran 𝑍 = ran (𝑡 ∘ 𝑅))
65	64	unieqd 4921	. . . . . . . 8 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran 𝑍 = ∪ ran (𝑡 ∘ 𝑅))
66	65	ineq1d 4210	. . . . . . 7 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈))
67	66	eqeq1d 2734	. . . . . 6 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → ((∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅ ↔ (∪ ran (𝑡 ∘ 𝑅) ∩ ∩ ran 𝑈) = ∅))
68	63, 67	imbitrrid 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 5933	. . . . . . . 8 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
72	71	unieqd 4921	. . . . . . 7 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → ∪ ran 𝑍 = ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
73	72	ineq1d 4210	. . . . . 6 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = (∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ∩ ∩ ran 𝑈))
74		rncoss 5969	. . . . . . . 8 ⊢ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
75	74	unissi 4916	. . . . . . 7 ⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
76		disj 4446	. . . . . . . 8 ⊢ ((∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅ ↔ ∀𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ¬ 𝑎 ∈ ∩ ran 𝑈)
77		eluniab 4922	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)} ↔ ∃𝑏(𝑎 ∈ 𝑏 ∧ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
78		eleq2 2822	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)))
79		eldifn 4126	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → ¬ 𝑎 ∈ ∩ ran 𝑈)
80	78, 79	syl6bi 252	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈) → (𝑎 ∈ 𝑏 → ¬ 𝑎 ∈ ∩ ran 𝑈))
81	80	rexlimivw 3151	. . . . . . . . . . . 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 2732	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
86	85	rnmpt 5952	. . . . . . . . . 10 ⊢ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
87	86	unieqi 4920	. . . . . . . . 9 ⊢ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = ∪ {𝑏 ∣ ∃𝑧 ∈ 𝑃 𝑏 = ((𝑡‘𝑧) ∖ ∩ ran 𝑈)}
88	84, 87	eleq2s 2851	. . . . . . . 8 ⊢ (𝑎 ∈ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) → ¬ 𝑎 ∈ ∩ ran 𝑈)
89	76, 88	mprgbir 3068	. . . . . . 7 ⊢ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∩ ∩ ran 𝑈) = ∅
90		ssdisj 4458	. . . . . . 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 2788	. . . . 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 𝑈) = ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∃wex 1781 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 {crab 3432 Vcvv 3474 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 𝒫 cpw 4601 ∪ cuni 4907 ∩ cint 4949 class class class wbr 5147 ↦ cmpt 5230 dom cdm 5675 ran crn 5676 ∘ ccom 5679 suc csuc 6363 Fun wfun 6534 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 ℩crio 7360 (class class class)co 7405 ∈ cmpo 7407 ωcom 7851 seq_ωcseqom 8443 ↑_m cmap 8816 ≈ cen 8932 Fincfn 8935

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 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

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 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 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 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-seqom 8444 df-1o 8462 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-card 9930

This theorem is referenced by: fin23lem31 10334

W3C validator