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 eqtr4di ( 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ 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 elrabi ( ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } → ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ 𝐵 )
46 45 ralimi ( ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } → ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ 𝐵 )
47 46 ad2antll ( ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) ) → ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ 𝐵 )
48 eqid ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
49 48 fmpt ( ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ 𝐵 ↔ ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) : 𝐴𝐵 )
50 47 49 sylib ( ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) ) → ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) : 𝐴𝐵 )
51 nfcv 𝑦 𝐵
52 51 elrabsf ( ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ↔ ( ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ 𝐵[ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) )
53 52 simprbi ( ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } → [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 )
54 53 ralimi ( ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } → ∀ 𝑥𝐴 [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 )
55 54 ad2antll ( ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) ) → ∀ 𝑥𝐴 [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 )
56 50 55 jca ( ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) ) → ( ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) : 𝐴𝐵 ∧ ∀ 𝑥𝐴 [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) )
57 feq1 ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) → ( 𝑓 : 𝐴𝐵 ↔ ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) : 𝐴𝐵 ) )
58 nfmpt1 𝑥 ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
59 58 nfeq2 𝑥 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
60 fvex ( 𝑓𝑥 ) ∈ V
61 60 1 sbcie ( [ ( 𝑓𝑥 ) / 𝑦 ] 𝜑𝜓 )
62 fveq1 ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) → ( 𝑓𝑥 ) = ( ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ‘ 𝑥 ) )
63 fvex ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ V
64 48 fvmpt2 ( ( 𝑥𝐴 ∧ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ V ) → ( ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ‘ 𝑥 ) = ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
65 63 64 mpan2 ( 𝑥𝐴 → ( ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ‘ 𝑥 ) = ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
66 62 65 sylan9eq ( ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ∧ 𝑥𝐴 ) → ( 𝑓𝑥 ) = ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) )
67 66 sbceq1d ( ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ∧ 𝑥𝐴 ) → ( [ ( 𝑓𝑥 ) / 𝑦 ] 𝜑[ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) )
68 61 67 bitr3id ( ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) ∧ 𝑥𝐴 ) → ( 𝜓[ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) )
69 59 68 ralbida ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥𝐴 [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) )
70 57 69 anbi12d ( 𝑓 = ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) → ( ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) ↔ ( ( 𝑥𝐴 ↦ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ) : 𝐴𝐵 ∧ ∀ 𝑥𝐴 [ ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) / 𝑦 ] 𝜑 ) ) )
71 44 56 70 spcedv ( ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) ∧ ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) )
72 71 ex ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) → ( ( 𝑔 Fn ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑥𝐴 ( 𝑔 ‘ { 𝑦𝐵𝜑 } ) ∈ { 𝑦𝐵𝜑 } ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) ) )
73 42 72 syld ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) → ( ( 𝑔 : ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ⟶ ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ( 𝑔𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) ) )
74 73 exlimdv ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) → ( ∃ 𝑔 ( 𝑔 : ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ⟶ ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ∧ ∀ 𝑧 ∈ ran ( 𝑥𝐴 ↦ { 𝑦𝐵𝜑 } ) ( 𝑔𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) ) )
75 32 74 mpd ( ( 𝐴𝑉 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) )