Metamath Proof Explorer

Theorem ac6num

Description: A version of ac6 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis ac6num.1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion ac6num ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ac6num.1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
2 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
3 2 nfel1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card
4 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
5 ssexg ⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ) → { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V )
6 5 expcom ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } → { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V ) )
7 4 6 syl5 ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ( 𝑥 ∈ 𝐴 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V ) )
8 3 7 ralrimi ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V )
9 dfiun2g ⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } } )
10 8 9 syl ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } } )
11 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
12 11 rnmpt ⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } }
13 12 unieqi ⊢ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } }
14 10 13 syl6eqr ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
15 id ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card )
16 14 15 eqeltrrd ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card → ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ dom card )
17 16 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ dom card )
18 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
19 necom ⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ↔ ∅ ≠ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
20 rabn0 ⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝐵 𝜑 )
21 df-ne ⊢ ( ∅ ≠ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ¬ ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
22 19 20 21 3bitr3i ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
23 22 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
24 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
25 23 24 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
26 18 25 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ¬ ∃ 𝑥 ∈ 𝐴 ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
27 0ex ⊢ ∅ ∈ V
28 11 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ↔ ∃ 𝑥 ∈ 𝐴 ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
29 27 28 ax-mp ⊢ ( ∅ ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ↔ ∃ 𝑥 ∈ 𝐴 ∅ = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
30 26 29 sylnibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ¬ ∅ ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
31 ac5num ⊢ ( ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ dom card ∧ ¬ ∅ ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ∃ 𝑔 ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
32 17 30 31 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑔 ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
33 ffn ⊢ ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) → 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
34 33 anim1i ⊢ ( ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
35 8 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V )
36 fveq2 ⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( 𝑔 ‘ 𝑧 ) = ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
37 id ⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
38 36 37 eleq12d ⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
39 11 38 ralrnmptw ⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
40 35 39 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
41 40 anbi2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) )
42 34 41 syl5ib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) )
43 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → 𝐴 ∈ 𝑉 )
44 43 mptexd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ∈ V )
45 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵
46 45 sseli ⊢ ( ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ 𝐵 )
47 46 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ 𝐵 )
48 47 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ 𝐵 )
49 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
50 49 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) : 𝐴 ⟶ 𝐵 )
51 48 50 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) : 𝐴 ⟶ 𝐵 )
52 nfcv ⊢ Ⅎ 𝑦 𝐵
53 52 elrabsf ⊢ ( ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ( ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ 𝐵 ∧ [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) )
54 53 simprbi ⊢ ( ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 )
55 54 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ∀ 𝑥 ∈ 𝐴 [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 )
56 55 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ∀ 𝑥 ∈ 𝐴 [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 )
57 51 56 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) )
58 feq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) : 𝐴 ⟶ 𝐵 ) )
59 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
60 59 nfeq2 ⊢ Ⅎ 𝑥 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
61 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
62 61 1 sbcie ⊢ ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ 𝜓 )
63 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ‘ 𝑥 ) )
64 fvex ⊢ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ V
65 49 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ‘ 𝑥 ) = ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
66 64 65 mpan2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ‘ 𝑥 ) = ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
67 63 66 sylan9eq ⊢ ( ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
68 67 sbceq1d ⊢ ( ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) )
69 62 68 syl5bbr ⊢ ( ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) )
70 60 69 ralbida ⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) )
71 58 70 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) / 𝑦 ] 𝜑 ) ) )
72 44 57 71 spcedv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
73 72 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
74 42 73 syld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
75 74 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃ 𝑔 ( 𝑔 : ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ⟶ ∪ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
76 32 75 mpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )