Theorem fin23lem28 10096

Description: Lemma for fin23 10145. 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 4500	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	1, 2	mpbi 229	. 2 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))
4		difss 4066	. . . . . . . . 9 ⊢ (ω ∖ 𝑃) ⊆ ω
5		ominf 9035	. . . . . . . . . 10 ⊢ ¬ ω ∈ Fin
6		fin23lem.b	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
7	6	ssrab3 4015	. . . . . . . . . . . . 13 ⊢ 𝑃 ⊆ ω
8		undif 4415	. . . . . . . . . . . . 13 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
9	7, 8	mpbi 229	. . . . . . . . . . . 12 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
10		unfi 8955	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
11	9, 10	eqeltrrid 2844	. . . . . . . . . . 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 10083	. . . . . . . . 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 6715	. . . . . . 7 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω–1-1→(ω ∖ 𝑃))
19		f1ss 6676	. . . . . . . 8 ⊢ ((𝑅:ω–1-1→(ω ∖ 𝑃) ∧ (ω ∖ 𝑃) ⊆ ω) → 𝑅:ω–1-1→ω)
20	4, 19	mpan2 688	. . . . . . 7 ⊢ (𝑅:ω–1-1→(ω ∖ 𝑃) → 𝑅:ω–1-1→ω)
21	17, 18, 20	3syl 18	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1→ω)
22		f1co 6682	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑅:ω–1-1→ω) → (𝑡 ∘ 𝑅):ω–1-1→V)
23	21, 22	syldan 591	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑡 ∘ 𝑅):ω–1-1→V)
24		f1eq1 6665	. . . . 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 6787	. . . . . . . . . . 11 ⊢ (𝑡‘𝑧) ∈ V
28	27	difexi 5252	. . . . . . . . . 10 ⊢ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
29	28	rgenw 3076	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
30		eqid 2738	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
31	30	fmpt 6984	. . . . . . . . 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 6774	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝑡‘𝑧) = (𝑡‘𝑎))
35	34	difeq1d 4056	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
36		fvex 6787	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑎) ∈ V
37	36	difexi 5252	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) ∈ V
38	35, 30, 37	fvmpt 6875	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
39	38	ad2antrl 725	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
40		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑏 → (𝑡‘𝑧) = (𝑡‘𝑏))
41	40	difeq1d 4056	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑏 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
42		fvex 6787	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑏) ∈ V
43	42	difexi 5252	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑏) ∖ ∩ ran 𝑈) ∈ V
44	41, 30, 43	fvmpt 6875	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
45	44	ad2antll 726	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
46	39, 45	eqeq12d 2754	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) ↔ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
47		uneq2 4091	. . . . . . . . . . 11 ⊢ (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
48		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → (𝑡‘𝑣) = (𝑡‘𝑎))
49	48	sseq2d 3953	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
50	49, 6	elrab2 3627	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝑃 ↔ (𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
51	50	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
52	51	ad2antrl 725	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
53		undif 4415	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑎) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
54	52, 53	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
55		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑏 → (𝑡‘𝑣) = (𝑡‘𝑏))
56	55	sseq2d 3953	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑏 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
57	56, 6	elrab2 3627	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑃 ↔ (𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
58	57	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
59	58	ad2antll 726	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
60		undif 4415	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑏) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
61	59, 60	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
62	54, 61	eqeq12d 2754	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) ↔ (𝑡‘𝑎) = (𝑡‘𝑏)))
63	47, 62	syl5ib 243	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (𝑡‘𝑎) = (𝑡‘𝑏)))
64	7	sseli 3917	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑃 → 𝑎 ∈ ω)
65	7	sseli 3917	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑃 → 𝑏 ∈ ω)
66	64, 65	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (𝑎 ∈ ω ∧ 𝑏 ∈ ω))
67		f1fveq 7135	. . . . . . . . . . 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 3123	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
72		dff13 7128	. . . . . . 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 10083	. . . . . . . 8 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1-onto→𝑃)
76		f1of1 6715	. . . . . . . 8 ⊢ (𝑄:ω–1-1-onto→𝑃 → 𝑄:ω–1-1→𝑃)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1→𝑃)
78	7, 77	mpan 687	. . . . . 6 ⊢ (¬ 𝑃 ∈ Fin → 𝑄:ω–1-1→𝑃)
79		f1co 6682	. . . . . 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 6665	. . . . 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 955	. 2 ⊢ ((𝑡:ω–1-1→V ∧ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))) → 𝑍:ω–1-1→V)
85	3, 84	mpan2 688	1 ⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106  {cab 2715  ∀wral 3064  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459  𝒫 cpw 4533  ∪ cuni 4839  ∩ cint 4879   class class class wbr 5074   ↦ cmpt 5157  ran crn 5590   ∘ ccom 5593  suc csuc 6268  ⟶wf 6429  –1-1→wf1 6430  –1-1-onto→wf1o 6432  ‘cfv 6433  ℩crio 7231  (class class class)co 7275   ∈ cmpo 7277  ωcom 7712  seq_ωcseqom 8278   ↑_m cmap 8615   ≈ cen 8730  Fincfn 8733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-card 9697

This theorem is referenced by:  fin23lem32  10100