Theorem aceq3lem

Description: Lemma for dfac3 . (Contributed by NM, 2-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypothesis	aceq3lem.1	⊢ 𝐹 = ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
Assertion	aceq3lem	⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		aceq3lem.1	⊢ 𝐹 = ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
2		vex	⊢ 𝑦 ∈ V
3	2	rnex	⊢ ran 𝑦 ∈ V
4	3	pwex	⊢ 𝒫 ran 𝑦 ∈ V
5		raleq	⊢ ( 𝑥 = 𝒫 ran 𝑦 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
6	5	exbidv	⊢ ( 𝑥 = 𝒫 ran 𝑦 → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
7	4 6	spcv	⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
8		df-mpt	⊢ ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) = { ⟨ 𝑤 , ℎ ⟩ ∣ ( 𝑤 ∈ dom 𝑦 ∧ ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) }
9	1 8	eqtri	⊢ 𝐹 = { ⟨ 𝑤 , ℎ ⟩ ∣ ( 𝑤 ∈ dom 𝑦 ∧ ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) }
10		vex	⊢ 𝑤 ∈ V
11	10	eldm	⊢ ( 𝑤 ∈ dom 𝑦 ↔ ∃ 𝑢 𝑤 𝑦 𝑢 )
12		abn0	⊢ ( { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ ↔ ∃ 𝑢 𝑤 𝑦 𝑢 )
13	11 12	bitr4i	⊢ ( 𝑤 ∈ dom 𝑦 ↔ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ )
14		vex	⊢ 𝑢 ∈ V
15	10 14	brelrn	⊢ ( 𝑤 𝑦 𝑢 → 𝑢 ∈ ran 𝑦 )
16	15	abssi	⊢ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ⊆ ran 𝑦
17	3 16	elpwi2	⊢ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ∈ 𝒫 ran 𝑦
18		neeq1	⊢ ( 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } → ( 𝑧 ≠ ∅ ↔ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ ) )
19		fveq2	⊢ ( 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
20		id	⊢ ( 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } → 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } )
21	19 20	eleq12d	⊢ ( 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
22	18 21	imbi12d	⊢ ( 𝑧 = { 𝑢 ∣ 𝑤 𝑦 𝑢 } → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ → ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) )
23	22	rspcv	⊢ ( { 𝑢 ∣ 𝑤 𝑦 𝑢 } ∈ 𝒫 ran 𝑦 → ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ → ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) )
24	17 23	ax-mp	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( { 𝑢 ∣ 𝑤 𝑦 𝑢 } ≠ ∅ → ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
25	13 24	syl5bi	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑤 ∈ dom 𝑦 → ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
26	25	imp	⊢ ( ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ dom 𝑦 ) → ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } )
27		fvex	⊢ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ V
28		breq2	⊢ ( 𝑧 = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) → ( 𝑤 𝑦 𝑧 ↔ 𝑤 𝑦 ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) )
29		breq2	⊢ ( 𝑢 = 𝑧 → ( 𝑤 𝑦 𝑢 ↔ 𝑤 𝑦 𝑧 ) )
30	29	cbvabv	⊢ { 𝑢 ∣ 𝑤 𝑦 𝑢 } = { 𝑧 ∣ 𝑤 𝑦 𝑧 }
31	27 28 30	elab2	⊢ ( ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ∈ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ↔ 𝑤 𝑦 ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
32	26 31	sylib	⊢ ( ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ dom 𝑦 ) → 𝑤 𝑦 ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
33		breq2	⊢ ( ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) → ( 𝑤 𝑦 ℎ ↔ 𝑤 𝑦 ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) )
34	32 33	syl5ibrcom	⊢ ( ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ dom 𝑦 ) → ( ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) → 𝑤 𝑦 ℎ ) )
35	34	expimpd	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑤 ∈ dom 𝑦 ∧ ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) → 𝑤 𝑦 ℎ ) )
36	35	ssopab2dv	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → { ⟨ 𝑤 , ℎ ⟩ ∣ ( 𝑤 ∈ dom 𝑦 ∧ ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) } ⊆ { ⟨ 𝑤 , ℎ ⟩ ∣ 𝑤 𝑦 ℎ } )
37		opabss	⊢ { ⟨ 𝑤 , ℎ ⟩ ∣ 𝑤 𝑦 ℎ } ⊆ 𝑦
38	36 37	sstrdi	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → { ⟨ 𝑤 , ℎ ⟩ ∣ ( 𝑤 ∈ dom 𝑦 ∧ ℎ = ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) } ⊆ 𝑦 )
39	9 38	eqsstrid	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → 𝐹 ⊆ 𝑦 )
40	27 1	fnmpti	⊢ 𝐹 Fn dom 𝑦
41	2	ssex	⊢ ( 𝐹 ⊆ 𝑦 → 𝐹 ∈ V )
42	41	adantr	⊢ ( ( 𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦 ) → 𝐹 ∈ V )
43		sseq1	⊢ ( 𝑔 = 𝐹 → ( 𝑔 ⊆ 𝑦 ↔ 𝐹 ⊆ 𝑦 ) )
44		fneq1	⊢ ( 𝑔 = 𝐹 → ( 𝑔 Fn dom 𝑦 ↔ 𝐹 Fn dom 𝑦 ) )
45	43 44	anbi12d	⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ↔ ( 𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦 ) ) )
46	45	spcegv	⊢ ( 𝐹 ∈ V → ( ( 𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦 ) → ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ) )
47	42 46	mpcom	⊢ ( ( 𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦 ) → ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) )
48	39 40 47	sylancl	⊢ ( ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) )
49	48	exlimiv	⊢ ( ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 ran 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) )
50	7 49	syl	⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) )
51		sseq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ⊆ 𝑦 ↔ 𝑓 ⊆ 𝑦 ) )
52		fneq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 Fn dom 𝑦 ↔ 𝑓 Fn dom 𝑦 ) )
53	51 52	anbi12d	⊢ ( 𝑔 = 𝑓 → ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ↔ ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ) )
54	53	cbvexvw	⊢ ( ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )
55	50 54	sylib	⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )