This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( ∀ 𝑧 ∈ 𝒫 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 𝑦 ) )