Theorem fin23lem28 10352

Description: Lemma for fin23 10401. 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 4542	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	1, 2	mpbi 230	. 2 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))
4		difss 4111	. . . . . . . . 9 ⊢ (ω ∖ 𝑃) ⊆ ω
5		ominf 9264	. . . . . . . . . 10 ⊢ ¬ ω ∈ Fin
6		fin23lem.b	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
7	6	ssrab3 4057	. . . . . . . . . . . . 13 ⊢ 𝑃 ⊆ ω
8		undif 4457	. . . . . . . . . . . . 13 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
9	7, 8	mpbi 230	. . . . . . . . . . . 12 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
10		unfi 9183	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
11	9, 10	eqeltrrid 2839	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → ω ∈ Fin)
12	11	ex 412	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → ((ω ∖ 𝑃) ∈ Fin → ω ∈ Fin))
13	5, 12	mtoi 199	. . . . . . . . 9 ⊢ (𝑃 ∈ Fin → ¬ (ω ∖ 𝑃) ∈ Fin)
14		fin23lem.d	. . . . . . . . . 10 ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
15	14	fin23lem22 10339	. . . . . . . . 9 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
16	4, 13, 15	sylancr 587	. . . . . . . 8 ⊢ (𝑃 ∈ Fin → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
17	16	adantl 481	. . . . . . 7 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
18		f1of1 6816	. . . . . . 7 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω–1-1→(ω ∖ 𝑃))
19		f1ss 6778	. . . . . . . 8 ⊢ ((𝑅:ω–1-1→(ω ∖ 𝑃) ∧ (ω ∖ 𝑃) ⊆ ω) → 𝑅:ω–1-1→ω)
20	4, 19	mpan2 691	. . . . . . 7 ⊢ (𝑅:ω–1-1→(ω ∖ 𝑃) → 𝑅:ω–1-1→ω)
21	17, 18, 20	3syl 18	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1→ω)
22		f1co 6784	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑅:ω–1-1→ω) → (𝑡 ∘ 𝑅):ω–1-1→V)
23	21, 22	syldan 591	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑡 ∘ 𝑅):ω–1-1→V)
24		f1eq1 6768	. . . . 5 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (𝑍:ω–1-1→V ↔ (𝑡 ∘ 𝑅):ω–1-1→V))
25	23, 24	syl5ibrcom 247	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑍 = (𝑡 ∘ 𝑅) → 𝑍:ω–1-1→V))
26	25	impr 454	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅))) → 𝑍:ω–1-1→V)
27		fvex 6888	. . . . . . . . . . 11 ⊢ (𝑡‘𝑧) ∈ V
28	27	difexi 5300	. . . . . . . . . 10 ⊢ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
29	28	rgenw 3055	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
30		eqid 2735	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
31	30	fmpt 7099	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V ↔ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
32	29, 31	mpbi 230	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V
33	32	a1i 11	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
34		fveq2 6875	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝑡‘𝑧) = (𝑡‘𝑎))
35	34	difeq1d 4100	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
36		fvex 6888	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑎) ∈ V
37	36	difexi 5300	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) ∈ V
38	35, 30, 37	fvmpt 6985	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
39	38	ad2antrl 728	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
40		fveq2 6875	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑏 → (𝑡‘𝑧) = (𝑡‘𝑏))
41	40	difeq1d 4100	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑏 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
42		fvex 6888	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑏) ∈ V
43	42	difexi 5300	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑏) ∖ ∩ ran 𝑈) ∈ V
44	41, 30, 43	fvmpt 6985	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
45	44	ad2antll 729	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
46	39, 45	eqeq12d 2751	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) ↔ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
47		uneq2 4137	. . . . . . . . . . 11 ⊢ (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
48		fveq2 6875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → (𝑡‘𝑣) = (𝑡‘𝑎))
49	48	sseq2d 3991	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
50	49, 6	elrab2 3674	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝑃 ↔ (𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
51	50	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
52	51	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
53		undif 4457	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑎) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
54	52, 53	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
55		fveq2 6875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑏 → (𝑡‘𝑣) = (𝑡‘𝑏))
56	55	sseq2d 3991	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑏 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
57	56, 6	elrab2 3674	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑃 ↔ (𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
58	57	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
59	58	ad2antll 729	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
60		undif 4457	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑏) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
61	59, 60	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
62	54, 61	eqeq12d 2751	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) ↔ (𝑡‘𝑎) = (𝑡‘𝑏)))
63	47, 62	imbitrid 244	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (𝑡‘𝑎) = (𝑡‘𝑏)))
64	7	sseli 3954	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑃 → 𝑎 ∈ ω)
65	7	sseli 3954	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑃 → 𝑏 ∈ ω)
66	64, 65	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (𝑎 ∈ ω ∧ 𝑏 ∈ ω))
67		f1fveq 7254	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
68	66, 67	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
69	63, 68	sylibd 239	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → 𝑎 = 𝑏))
70	46, 69	sylbid 240	. . . . . . . 8 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
71	70	ralrimivva 3187	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
72		dff13 7246	. . . . . . 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 10339	. . . . . . . 8 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1-onto→𝑃)
76		f1of1 6816	. . . . . . . 8 ⊢ (𝑄:ω–1-1-onto→𝑃 → 𝑄:ω–1-1→𝑃)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1→𝑃)
78	7, 77	mpan 690	. . . . . 6 ⊢ (¬ 𝑃 ∈ Fin → 𝑄:ω–1-1→𝑃)
79		f1co 6784	. . . . . 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 6768	. . . . 5 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (𝑍:ω–1-1→V ↔ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V))
82	80, 81	syl5ibrcom 247	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ ¬ 𝑃 ∈ Fin) → (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → 𝑍:ω–1-1→V))
83	82	impr 454	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))) → 𝑍:ω–1-1→V)
84	26, 83	jaodan 959	. 2 ⊢ ((𝑡:ω–1-1→V ∧ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))) → 𝑍:ω–1-1→V)
85	3, 84	mpan2 691	1 ⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108  {cab 2713  ∀wral 3051  {crab 3415  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  ifcif 4500  𝒫 cpw 4575  ∪ cuni 4883  ∩ cint 4922   class class class wbr 5119   ↦ cmpt 5201  ran crn 5655   ∘ ccom 5658  suc csuc 6354  ⟶wf 6526  –1-1→wf1 6527  –1-1-onto→wf1o 6529  ‘cfv 6530  ℩crio 7359  (class class class)co 7403   ∈ cmpo 7405  ωcom 7859  seq_ωcseqom 8459   ↑_m cmap 8838   ≈ cen 8954  Fincfn 8957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-1o 8478  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-card 9951

This theorem is referenced by:  fin23lem32  10356