Metamath Proof Explorer

Theorem acnlem

Description: Construct a mapping satisfying the consequent of isacn . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnlem ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ f ⁡ x → ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢ f ⁡ x ⊆ ⋃ ran ⁡ f
2 simpr ⊢ x ∈ A ∧ B ∈ f ⁡ x → B ∈ f ⁡ x
3 1 2 sselid ⊢ x ∈ A ∧ B ∈ f ⁡ x → B ∈ ⋃ ran ⁡ f
4 3 ralimiaa ⊢ ∀ x ∈ A B ∈ f ⁡ x → ∀ x ∈ A B ∈ ⋃ ran ⁡ f
5 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
6 5 fmpt ⊢ ∀ x ∈ A B ∈ ⋃ ran ⁡ f ↔ x ∈ A ⟼ B : A ⟶ ⋃ ran ⁡ f
7 4 6 sylib ⊢ ∀ x ∈ A B ∈ f ⁡ x → x ∈ A ⟼ B : A ⟶ ⋃ ran ⁡ f
8 id ⊢ A ∈ V → A ∈ V
9 vex ⊢ f ∈ V
10 9 rnex ⊢ ran ⁡ f ∈ V
11 10 uniex ⊢ ⋃ ran ⁡ f ∈ V
12 fex2 ⊢ x ∈ A ⟼ B : A ⟶ ⋃ ran ⁡ f ∧ A ∈ V ∧ ⋃ ran ⁡ f ∈ V → x ∈ A ⟼ B ∈ V
13 11 12 mp3an3 ⊢ x ∈ A ⟼ B : A ⟶ ⋃ ran ⁡ f ∧ A ∈ V → x ∈ A ⟼ B ∈ V
14 7 8 13 syl2anr ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ f ⁡ x → x ∈ A ⟼ B ∈ V
15 5 fvmpt2 ⊢ x ∈ A ∧ B ∈ f ⁡ x → x ∈ A ⟼ B ⁡ x = B
16 15 2 eqeltrd ⊢ x ∈ A ∧ B ∈ f ⁡ x → x ∈ A ⟼ B ⁡ x ∈ f ⁡ x
17 16 ralimiaa ⊢ ∀ x ∈ A B ∈ f ⁡ x → ∀ x ∈ A x ∈ A ⟼ B ⁡ x ∈ f ⁡ x
18 17 adantl ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ f ⁡ x → ∀ x ∈ A x ∈ A ⟼ B ⁡ x ∈ f ⁡ x
19 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
20 19 nfeq2 ⊢ Ⅎ x g = x ∈ A ⟼ B
21 fveq1 ⊢ g = x ∈ A ⟼ B → g ⁡ x = x ∈ A ⟼ B ⁡ x
22 21 eleq1d ⊢ g = x ∈ A ⟼ B → g ⁡ x ∈ f ⁡ x ↔ x ∈ A ⟼ B ⁡ x ∈ f ⁡ x
23 20 22 ralbid ⊢ g = x ∈ A ⟼ B → ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∀ x ∈ A x ∈ A ⟼ B ⁡ x ∈ f ⁡ x
24 14 18 23 spcedv ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ f ⁡ x → ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x