Theorem fin23lem28 10324

Description: Lemma for fin23 10373. 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 4534	. . 3 ⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))))
3	1, 2	mpbi 233	. 2 ⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))
4		difss 4098	. . . . . . . . 9 ⊢ (ω ∖ 𝑃) ⊆ ω
5		ominf 9224	. . . . . . . . . 10 ⊢ ¬ ω ∈ Fin
6		fin23lem.b	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}
7	6	ssrab3 4044	. . . . . . . . . . . . 13 ⊢ 𝑃 ⊆ ω
8		undif 4448	. . . . . . . . . . . . 13 ⊢ (𝑃 ⊆ ω ↔ (𝑃 ∪ (ω ∖ 𝑃)) = ω)
9	7, 8	mpbi 233	. . . . . . . . . . . 12 ⊢ (𝑃 ∪ (ω ∖ 𝑃)) = ω
10		unfi 9155	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → (𝑃 ∪ (ω ∖ 𝑃)) ∈ Fin)
11	9, 10	eqeltrrid 2874	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Fin ∧ (ω ∖ 𝑃) ∈ Fin) → ω ∈ Fin)
12	11	ex 417	. . . . . . . . . 10 ⊢ (𝑃 ∈ Fin → ((ω ∖ 𝑃) ∈ Fin → ω ∈ Fin))
13	5, 12	mtoi 202	. . . . . . . . 9 ⊢ (𝑃 ∈ Fin → ¬ (ω ∖ 𝑃) ∈ Fin)
14		fin23lem.d	. . . . . . . . . 10 ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
15	14	fin23lem22 10311	. . . . . . . . 9 ⊢ (((ω ∖ 𝑃) ⊆ ω ∧ ¬ (ω ∖ 𝑃) ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
16	4, 13, 15	sylancr 598	. . . . . . . 8 ⊢ (𝑃 ∈ Fin → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
17	16	adantl 486	. . . . . . 7 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1-onto→(ω ∖ 𝑃))
18		f1of1 6820	. . . . . . 7 ⊢ (𝑅:ω–1-1-onto→(ω ∖ 𝑃) → 𝑅:ω–1-1→(ω ∖ 𝑃))
19		f1ss 6782	. . . . . . . 8 ⊢ ((𝑅:ω–1-1→(ω ∖ 𝑃) ∧ (ω ∖ 𝑃) ⊆ ω) → 𝑅:ω–1-1→ω)
20	4, 19	mpan2 703	. . . . . . 7 ⊢ (𝑅:ω–1-1→(ω ∖ 𝑃) → 𝑅:ω–1-1→ω)
21	17, 18, 20	3syl 19	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → 𝑅:ω–1-1→ω)
22		f1co 6788	. . . . . 6 ⊢ ((𝑡:ω–1-1→V ∧ 𝑅:ω–1-1→ω) → (𝑡 ∘ 𝑅):ω–1-1→V)
23	21, 22	syldan 602	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑡 ∘ 𝑅):ω–1-1→V)
24		f1eq1 6770	. . . . 5 ⊢ (𝑍 = (𝑡 ∘ 𝑅) → (𝑍:ω–1-1→V ↔ (𝑡 ∘ 𝑅):ω–1-1→V))
25	23, 24	syl5ibrcom 250	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ 𝑃 ∈ Fin) → (𝑍 = (𝑡 ∘ 𝑅) → 𝑍:ω–1-1→V))
26	25	impr 459	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅))) → 𝑍:ω–1-1→V)
27		fvex 6895	. . . . . . . . . . 11 ⊢ (𝑡‘𝑧) ∈ V
28	27	difexi 5301	. . . . . . . . . 10 ⊢ ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
29	28	rgenw 3089	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V
30		eqid 2769	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))
31	30	fmpt 7106	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑃 ((𝑡‘𝑧) ∖ ∩ ran 𝑈) ∈ V ↔ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
32	29, 31	mpbi 233	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V
33	32	a1i 11	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V)
34		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝑡‘𝑧) = (𝑡‘𝑎))
35	34	difeq1d 4088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
36		fvex 6895	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑎) ∈ V
37	36	difexi 5301	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) ∈ V
38	35, 30, 37	fvmpt 6990	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
39	38	ad2antrl 740	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑡‘𝑎) ∖ ∩ ran 𝑈))
40		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑏 → (𝑡‘𝑧) = (𝑡‘𝑏))
41	40	difeq1d 4088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑏 → ((𝑡‘𝑧) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
42		fvex 6895	. . . . . . . . . . . . 13 ⊢ (𝑡‘𝑏) ∈ V
43	42	difexi 5301	. . . . . . . . . . . 12 ⊢ ((𝑡‘𝑏) ∖ ∩ ran 𝑈) ∈ V
44	41, 30, 43	fvmpt 6990	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑃 → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
45	44	ad2antll 741	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈))
46	39, 45	eqeq12d 2785	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) ↔ ((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
47		uneq2 4124	. . . . . . . . . . 11 ⊢ (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)))
48		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → (𝑡‘𝑣) = (𝑡‘𝑎))
49	48	sseq2d 3977	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
50	49, 6	elrab2 3663	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝑃 ↔ (𝑎 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑎)))
51	50	simprbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
52	51	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑎))
53		undif 4448	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑎) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
54	52, 53	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (𝑡‘𝑎))
55		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑏 → (𝑡‘𝑣) = (𝑡‘𝑏))
56	55	sseq2d 3977	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑏 → (∩ ran 𝑈 ⊆ (𝑡‘𝑣) ↔ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
57	56, 6	elrab2 3663	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑃 ↔ (𝑏 ∈ ω ∧ ∩ ran 𝑈 ⊆ (𝑡‘𝑏)))
58	57	simprbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝑃 → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
59	58	ad2antll 741	. . . . . . . . . . . . 13 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∩ ran 𝑈 ⊆ (𝑡‘𝑏))
60		undif 4448	. . . . . . . . . . . . 13 ⊢ (∩ ran 𝑈 ⊆ (𝑡‘𝑏) ↔ (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
61	59, 60	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) = (𝑡‘𝑏))
62	54, 61	eqeq12d 2785	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((∩ ran 𝑈 ∪ ((𝑡‘𝑎) ∖ ∩ ran 𝑈)) = (∩ ran 𝑈 ∪ ((𝑡‘𝑏) ∖ ∩ ran 𝑈)) ↔ (𝑡‘𝑎) = (𝑡‘𝑏)))
63	47, 62	imbitrid 247	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → (𝑡‘𝑎) = (𝑡‘𝑏)))
64	7	sseli 3941	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑃 → 𝑎 ∈ ω)
65	7	sseli 3941	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑃 → 𝑏 ∈ ω)
66	64, 65	anim12i 624	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (𝑎 ∈ ω ∧ 𝑏 ∈ ω))
67		f1fveq 7261	. . . . . . . . . . 11 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
68	66, 67	sylan2 604	. . . . . . . . . 10 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑡‘𝑎) = (𝑡‘𝑏) ↔ 𝑎 = 𝑏))
69	63, 68	sylibd 242	. . . . . . . . 9 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑡‘𝑎) ∖ ∩ ran 𝑈) = ((𝑡‘𝑏) ∖ ∩ ran 𝑈) → 𝑎 = 𝑏))
70	46, 69	sylbid 243	. . . . . . . 8 ⊢ ((𝑡:ω–1-1→V ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
71	70	ralrimivva 3214	. . . . . . 7 ⊢ (𝑡:ω–1-1→V → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏))
72		dff13 7253	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V ↔ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃⟶V ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑎) = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈))‘𝑏) → 𝑎 = 𝑏)))
73	33, 71, 72	sylanbrc 594	. . . . . 6 ⊢ (𝑡:ω–1-1→V → (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V)
74		fin23lem.c	. . . . . . . . 9 ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))
75	74	fin23lem22 10311	. . . . . . . 8 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1-onto→𝑃)
76		f1of1 6820	. . . . . . . 8 ⊢ (𝑄:ω–1-1-onto→𝑃 → 𝑄:ω–1-1→𝑃)
77	75, 76	syl 18	. . . . . . 7 ⊢ ((𝑃 ⊆ ω ∧ ¬ 𝑃 ∈ Fin) → 𝑄:ω–1-1→𝑃)
78	7, 77	mpan 702	. . . . . 6 ⊢ (¬ 𝑃 ∈ Fin → 𝑄:ω–1-1→𝑃)
79		f1co 6788	. . . . . 6 ⊢ (((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)):𝑃–1-1→V ∧ 𝑄:ω–1-1→𝑃) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V)
80	73, 78, 79	syl2an 607	. . . . 5 ⊢ ((𝑡:ω–1-1→V ∧ ¬ 𝑃 ∈ Fin) → ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V)
81		f1eq1 6770	. . . . 5 ⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → (𝑍:ω–1-1→V ↔ ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄):ω–1-1→V))
82	80, 81	syl5ibrcom 250	. . . 4 ⊢ ((𝑡:ω–1-1→V ∧ ¬ 𝑃 ∈ Fin) → (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄) → 𝑍:ω–1-1→V))
83	82	impr 459	. . 3 ⊢ ((𝑡:ω–1-1→V ∧ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))) → 𝑍:ω–1-1→V)
84	26, 83	jaodan 972	. 2 ⊢ ((𝑡:ω–1-1→V ∧ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)))) → 𝑍:ω–1-1→V)
85	3, 84	mpan2 703	1 ⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149  {cab 2747  ∀wral 3085  {crab 3423  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  ifcif 4492  𝒫 cpw 4567  ∪ cuni 4876  ∩ cint 4916   class class class wbr 5113   ↦ cmpt 5196  ran crn 5663   ∘ ccom 5666  suc csuc 6363  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537  ℩crio 7367  (class class class)co 7411   ∈ cmpo 7413  ωcom 7862  seq_ωcseqom 8434   ↑_m cmap 8824   ≈ cen 8940  Fincfn 8943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-1o 8453  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-card 9925

This theorem is referenced by:  fin23lem32  10328