Theorem fin23lem28 10293

Description: Lemma for fin23 10342. 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 4530	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	1, 2	mpbi 230	. 2 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))
4		difss 4099	. . . . . . . . 9 ⊢ (ω ∖ 𝑃) ⊆ ω
5		ominf 9205	. . . . . . . . . 10 ⊢ ¬ ω ∈ Fin
6		fin23lem.b	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
7	6	ssrab3 4045	. . . . . . . . . . . . 13 ⊢ 𝑃 ⊆ ω
8		undif 4445	. . . . . . . . . . . . 13 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
9	7, 8	mpbi 230	. . . . . . . . . . . 12 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
10		unfi 9135	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
11	9, 10	eqeltrrid 2833	. . . . . . . . . . 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 10280	. . . . . . . . 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 6799	. . . . . . 7 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω–1-1→(ω ∖ 𝑃))
19		f1ss 6761	. . . . . . . 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 6767	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑅:ω–1-1→ω) → (𝑡 ∘ 𝑅):ω–1-1→V)
23	21, 22	syldan 591	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑡 ∘ 𝑅):ω–1-1→V)
24		f1eq1 6751	. . . . 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 6871	. . . . . . . . . . 11 ⊢ (𝑡‘𝑧) ∈ V
28	27	difexi 5285	. . . . . . . . . 10 ⊢ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
29	28	rgenw 3048	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
30		eqid 2729	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
31	30	fmpt 7082	. . . . . . . . 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 6858	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝑡‘𝑧) = (𝑡‘𝑎))
35	34	difeq1d 4088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
36		fvex 6871	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑎) ∈ V
37	36	difexi 5285	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) ∈ V
38	35, 30, 37	fvmpt 6968	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
39	38	ad2antrl 728	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
40		fveq2 6858	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑏 → (𝑡‘𝑧) = (𝑡‘𝑏))
41	40	difeq1d 4088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑏 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
42		fvex 6871	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑏) ∈ V
43	42	difexi 5285	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑏) ∖ ∩ ran 𝑈) ∈ V
44	41, 30, 43	fvmpt 6968	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
45	44	ad2antll 729	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
46	39, 45	eqeq12d 2745	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) ↔ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
47		uneq2 4125	. . . . . . . . . . 11 ⊢ (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
48		fveq2 6858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → (𝑡‘𝑣) = (𝑡‘𝑎))
49	48	sseq2d 3979	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
50	49, 6	elrab2 3662	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝑃 ↔ (𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
51	50	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
52	51	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
53		undif 4445	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑎) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
54	52, 53	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
55		fveq2 6858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑏 → (𝑡‘𝑣) = (𝑡‘𝑏))
56	55	sseq2d 3979	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑏 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
57	56, 6	elrab2 3662	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑃 ↔ (𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
58	57	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
59	58	ad2antll 729	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
60		undif 4445	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑏) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
61	59, 60	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
62	54, 61	eqeq12d 2745	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) ↔ (𝑡‘𝑎) = (𝑡‘𝑏)))
63	47, 62	imbitrid 244	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (𝑡‘𝑎) = (𝑡‘𝑏)))
64	7	sseli 3942	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑃 → 𝑎 ∈ ω)
65	7	sseli 3942	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑃 → 𝑏 ∈ ω)
66	64, 65	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (𝑎 ∈ ω ∧ 𝑏 ∈ ω))
67		f1fveq 7237	. . . . . . . . . . 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 3180	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
72		dff13 7229	. . . . . . 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 10280	. . . . . . . 8 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1-onto→𝑃)
76		f1of1 6799	. . . . . . . 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 6767	. . . . . 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 6751	. . . . 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 2109  {cab 2707  ∀wral 3044  {crab 3405  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  ifcif 4488  𝒫 cpw 4563  ∪ cuni 4871  ∩ cint 4910   class class class wbr 5107   ↦ cmpt 5188  ran crn 5639   ∘ ccom 5642  suc csuc 6334  ⟶wf 6507  –1-1→wf1 6508  –1-1-onto→wf1o 6510  ‘cfv 6511  ℩crio 7343  (class class class)co 7387   ∈ cmpo 7389  ωcom 7842  seq_ωcseqom 8415   ↑_m cmap 8799   ≈ cen 8915  Fincfn 8918

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-1o 8434  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-card 9892

This theorem is referenced by:  fin23lem32  10297