Theorem ttukeylem3 9586

Description: Lemma for ttukey 9593. (Contributed by Mario Carneiro, 11-May-2015.)

Hypotheses

Ref	Expression
ttukeylem.1	⊢ (𝜑 → 𝐹:(card‘(∪ 𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵))
ttukeylem.2	⊢ (𝜑 → 𝐵 ∈ 𝐴)
ttukeylem.3	⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
ttukeylem.4	⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))))

Assertion

Ref	Expression
ttukeylem3	⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))

Distinct variable groups:   𝑥,𝑧,𝐶   𝑥,𝐺,𝑧   𝜑,𝑧   𝑥,𝐴,𝑧   𝑥,𝐵,𝑧   𝑥,𝐹,𝑧

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ttukeylem3

Step	Hyp	Ref	Expression
1		ttukeylem.4	. . . 4 ⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))))
2	1	tfr2 7698	. . 3 ⊢ (𝐶 ∈ On → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅))))‘(𝐺 ↾ 𝐶)))
3	2	adantl 473	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅))))‘(𝐺 ↾ 𝐶)))
4		eqidd 2766	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))))
5		simpr 477	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝑧 = (𝐺 ↾ 𝐶))
6	5	dmeqd 5494	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = dom (𝐺 ↾ 𝐶))
7	1	tfr1 7697	. . . . . . . . 9 ⊢ 𝐺 Fn On
8		onss 7188	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
9	8	ad2antlr 718	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝐶 ⊆ On)
10		fnssres 6182	. . . . . . . . 9 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺 ↾ 𝐶) Fn 𝐶)
11	7, 9, 10	sylancr 581	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐺 ↾ 𝐶) Fn 𝐶)
12		fndm 6168	. . . . . . . 8 ⊢ ((𝐺 ↾ 𝐶) Fn 𝐶 → dom (𝐺 ↾ 𝐶) = 𝐶)
13	11, 12	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom (𝐺 ↾ 𝐶) = 𝐶)
14	6, 13	eqtrd 2799	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = 𝐶)
15	14	unieqd 4604	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ dom 𝑧 = ∪ 𝐶)
16	14, 15	eqeq12d 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∪ dom 𝑧 ↔ 𝐶 = ∪ 𝐶))
17	14	eqeq1d 2767	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∅ ↔ 𝐶 = ∅))
18	5	rneqd 5521	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = ran (𝐺 ↾ 𝐶))
19		df-ima 5290	. . . . . . . 8 ⊢ (𝐺 “ 𝐶) = ran (𝐺 ↾ 𝐶)
20	18, 19	syl6eqr 2817	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = (𝐺 “ 𝐶))
21	20	unieqd 4604	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ ran 𝑧 = ∪ (𝐺 “ 𝐶))
22	17, 21	ifbieq2d 4268	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧) = if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)))
23	5, 15	fveq12d 6382	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝑧‘∪ dom 𝑧) = ((𝐺 ↾ 𝐶)‘∪ 𝐶))
24	15	fveq2d 6379	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐹‘∪ dom 𝑧) = (𝐹‘∪ 𝐶))
25	24	sneqd 4346	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → {(𝐹‘∪ dom 𝑧)} = {(𝐹‘∪ 𝐶)})
26	23, 25	uneq12d 3930	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}))
27	26	eleq1d 2829	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴 ↔ (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴))
28		eqidd 2766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∅ = ∅)
29	27, 25, 28	ifbieq12d 4270	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅) = if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))
30	23, 29	uneq12d 3930	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))
31	16, 22, 30	ifbieq12d 4270	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅))) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))
32		onuni 7191	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
33	32	ad3antlr 722	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ On)
34		sucidg 5986	. . . . . . . . 9 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
35	33, 34	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
36		eloni 5918	. . . . . . . . . . 11 ⊢ (𝐶 ∈ On → Ord 𝐶)
37	36	ad2antlr 718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → Ord 𝐶)
38		orduniorsuc 7228	. . . . . . . . . 10 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
39	37, 38	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
40	39	orcanai 1025	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
41	35, 40	eleqtrrd 2847	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
42		fvres 6394	. . . . . . 7 ⊢ (∪ 𝐶 ∈ 𝐶 → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶))
43	41, 42	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶))
44	43	uneq1d 3928	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) = ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}))
45	44	eleq1d 2829	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴))
46	45	ifbid 4265	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅) = if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))
47	43, 46	uneq12d 3930	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) = ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))
48	47	ifeq2da 4274	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))
49	31, 48	eqtrd 2799	. . 3 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅))) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))
50		fnfun 6166	. . . . 5 ⊢ (𝐺 Fn On → Fun 𝐺)
51	7, 50	ax-mp 5	. . . 4 ⊢ Fun 𝐺
52		simpr 477	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → 𝐶 ∈ On)
53		resfunexg 6672	. . . 4 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V)
54	51, 52, 53	sylancr 581	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V)
55		ttukeylem.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
56		elex 3365	. . . . . 6 ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ V)
57	55, 56	syl 17	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
58		funimaexg 6153	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V)
59	51, 58	mpan 681	. . . . . 6 ⊢ (𝐶 ∈ On → (𝐺 “ 𝐶) ∈ V)
60		uniexg 7153	. . . . . 6 ⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺 “ 𝐶) ∈ V)
61	59, 60	syl 17	. . . . 5 ⊢ (𝐶 ∈ On → ∪ (𝐺 “ 𝐶) ∈ V)
62		ifcl 4287	. . . . 5 ⊢ ((𝐵 ∈ V ∧ ∪ (𝐺 “ 𝐶) ∈ V) → if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V)
63	57, 61, 62	syl2an 589	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V)
64		fvex 6388	. . . . 5 ⊢ (𝐺‘∪ 𝐶) ∈ V
65		snex 5064	. . . . . 6 ⊢ {(𝐹‘∪ 𝐶)} ∈ V
66		0ex 4950	. . . . . 6 ⊢ ∅ ∈ V
67	65, 66	ifex 4291	. . . . 5 ⊢ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅) ∈ V
68	64, 67	unex 7154	. . . 4 ⊢ ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) ∈ V
69		ifcl 4287	. . . 4 ⊢ ((if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V ∧ ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) ∈ V) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈ V)
70	63, 68, 69	sylancl 580	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈ V)
71	4, 49, 54, 70	fvmptd 6477	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅))))‘(𝐺 ↾ 𝐶)) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))
72	3, 71	eqtrd 2799	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 873  ∀wal 1650   = wceq 1652   ∈ wcel 2155  Vcvv 3350   ∖ cdif 3729   ∪ cun 3730   ∩ cin 3731   ⊆ wss 3732  ∅c0 4079  ifcif 4243  𝒫 cpw 4315  {csn 4334  ∪ cuni 4594   ↦ cmpt 4888  dom cdm 5277  ran crn 5278   ↾ cres 5279   “ cima 5280  Ord word 5907  Oncon0 5908  suc csuc 5910  Fun wfun 6062   Fn wfn 6063  –1-1-onto→wf1o 6067  ‘cfv 6068  recscrecs 7671  Fincfn 8160  cardccrd 9012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-wrecs 7610  df-recs 7672

This theorem is referenced by:  ttukeylem4  9587  ttukeylem5  9588  ttukeylem6  9589  ttukeylem7  9590