Theorem fin23lem28 10234

Description: Lemma for fin23 10283. The residual is also one-to-one. This preserves the induction invariant. (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
fin23lem28	⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V)

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

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

Proof of Theorem fin23lem28

Dummy variable 𝑏 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fin23lem.e	. . 3 ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))
2		eqif 4525	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	1, 2	mpbi 229	. 2 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))
4		difss 4089	. . . . . . . . 9 ⊢ (ω ∖ 𝑃) ⊆ ω
5		ominf 9160	. . . . . . . . . 10 ⊢ ¬ ω ∈ Fin
6		fin23lem.b	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
7	6	ssrab3 4038	. . . . . . . . . . . . 13 ⊢ 𝑃 ⊆ ω
8		undif 4439	. . . . . . . . . . . . 13 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
9	7, 8	mpbi 229	. . . . . . . . . . . 12 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
10		unfi 9074	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
11	9, 10	eqeltrrid 2843	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → ω ∈ Fin)
12	11	ex 413	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → ((ω ∖ 𝑃) ∈ Fin → ω ∈ Fin))
13	5, 12	mtoi 198	. . . . . . . . 9 ⊢ (𝑃 ∈ Fin → ¬ (ω ∖ 𝑃) ∈ Fin)
14		fin23lem.d	. . . . . . . . . 10 ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
15	14	fin23lem22 10221	. . . . . . . . 9 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
16	4, 13, 15	sylancr 587	. . . . . . . 8 ⊢ (𝑃 ∈ Fin → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
17	16	adantl 482	. . . . . . 7 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
18		f1of1 6780	. . . . . . 7 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω–1-1→(ω ∖ 𝑃))
19		f1ss 6741	. . . . . . . 8 ⊢ ((𝑅:ω–1-1→(ω ∖ 𝑃) ∧ (ω ∖ 𝑃) ⊆ ω) → 𝑅:ω–1-1→ω)
20	4, 19	mpan2 689	. . . . . . 7 ⊢ (𝑅:ω–1-1→(ω ∖ 𝑃) → 𝑅:ω–1-1→ω)
21	17, 18, 20	3syl 18	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1→ω)
22		f1co 6747	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑅:ω–1-1→ω) → (𝑡 ∘ 𝑅):ω–1-1→V)
23	21, 22	syldan 591	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑡 ∘ 𝑅):ω–1-1→V)
24		f1eq1 6730	. . . . 5 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (𝑍:ω–1-1→V ↔ (𝑡 ∘ 𝑅):ω–1-1→V))
25	23, 24	syl5ibrcom 246	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑍 = (𝑡 ∘ 𝑅) → 𝑍:ω–1-1→V))
26	25	impr 455	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅))) → 𝑍:ω–1-1→V)
27		fvex 6852	. . . . . . . . . . 11 ⊢ (𝑡‘𝑧) ∈ V
28	27	difexi 5283	. . . . . . . . . 10 ⊢ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
29	28	rgenw 3066	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
30		eqid 2736	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
31	30	fmpt 7054	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V ↔ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
32	29, 31	mpbi 229	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V
33	32	a1i 11	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
34		fveq2 6839	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝑡‘𝑧) = (𝑡‘𝑎))
35	34	difeq1d 4079	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
36		fvex 6852	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑎) ∈ V
37	36	difexi 5283	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) ∈ V
38	35, 30, 37	fvmpt 6945	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
39	38	ad2antrl 726	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
40		fveq2 6839	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑏 → (𝑡‘𝑧) = (𝑡‘𝑏))
41	40	difeq1d 4079	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑏 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
42		fvex 6852	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑏) ∈ V
43	42	difexi 5283	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑏) ∖ ∩ ran 𝑈) ∈ V
44	41, 30, 43	fvmpt 6945	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
45	44	ad2antll 727	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
46	39, 45	eqeq12d 2752	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) ↔ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
47		uneq2 4115	. . . . . . . . . . 11 ⊢ (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
48		fveq2 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → (𝑡‘𝑣) = (𝑡‘𝑎))
49	48	sseq2d 3974	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
50	49, 6	elrab2 3646	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝑃 ↔ (𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
51	50	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
52	51	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
53		undif 4439	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑎) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
54	52, 53	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
55		fveq2 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑏 → (𝑡‘𝑣) = (𝑡‘𝑏))
56	55	sseq2d 3974	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑏 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
57	56, 6	elrab2 3646	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑃 ↔ (𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
58	57	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
59	58	ad2antll 727	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
60		undif 4439	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑏) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
61	59, 60	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
62	54, 61	eqeq12d 2752	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) ↔ (𝑡‘𝑎) = (𝑡‘𝑏)))
63	47, 62	imbitrid 243	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (𝑡‘𝑎) = (𝑡‘𝑏)))
64	7	sseli 3938	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑃 → 𝑎 ∈ ω)
65	7	sseli 3938	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑃 → 𝑏 ∈ ω)
66	64, 65	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (𝑎 ∈ ω ∧ 𝑏 ∈ ω))
67		f1fveq 7205	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
68	66, 67	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
69	63, 68	sylibd 238	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → 𝑎 = 𝑏))
70	46, 69	sylbid 239	. . . . . . . 8 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
71	70	ralrimivva 3195	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
72		dff13 7198	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V ↔ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏)))
73	33, 71, 72	sylanbrc 583	. . . . . 6 ⊢ (𝑡:ω–1-1→V → (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V)
74		fin23lem.c	. . . . . . . . 9 ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))
75	74	fin23lem22 10221	. . . . . . . 8 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1-onto→𝑃)
76		f1of1 6780	. . . . . . . 8 ⊢ (𝑄:ω–1-1-onto→𝑃 → 𝑄:ω–1-1→𝑃)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1→𝑃)
78	7, 77	mpan 688	. . . . . 6 ⊢ (¬ 𝑃 ∈ Fin → 𝑄:ω–1-1→𝑃)
79		f1co 6747	. . . . . 6 ⊢ (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V ∧ 𝑄:ω–1-1→𝑃) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V)
80	73, 78, 79	syl2an 596	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ ¬ 𝑃 ∈ Fin) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V)
81		f1eq1 6730	. . . . 5 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (𝑍:ω–1-1→V ↔ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V))
82	80, 81	syl5ibrcom 246	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ ¬ 𝑃 ∈ Fin) → (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → 𝑍:ω–1-1→V))
83	82	impr 455	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))) → 𝑍:ω–1-1→V)
84	26, 83	jaodan 956	. 2 ⊢ ((𝑡:ω–1-1→V ∧ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))) → 𝑍:ω–1-1→V)
85	3, 84	mpan2 689	1 ⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cab 2713  ∀wral 3062  {crab 3405  Vcvv 3443   ∖ cdif 3905   ∪ cun 3906   ∩ cin 3907   ⊆ wss 3908  ∅c0 4280  ifcif 4484  𝒫 cpw 4558  ∪ cuni 4863  ∩ cint 4905   class class class wbr 5103   ↦ cmpt 5186  ran crn 5632   ∘ ccom 5635  suc csuc 6317  ⟶wf 6489  –1-1→wf1 6490  –1-1-onto→wf1o 6492  ‘cfv 6493  ℩crio 7306  (class class class)co 7351   ∈ cmpo 7353  ωcom 7794  seq_ωcseqom 8385   ↑_m cmap 8723   ≈ cen 8838  Fincfn 8841

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 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664

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 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-om 7795  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-1o 8404  df-er 8606  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-card 9833

This theorem is referenced by:  fin23lem32  10238