Metamath Proof Explorer


Theorem smfpimcclem

Description: Lemma for smfpimcc given the choice function C . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfpimcclem.n 𝑛 𝜑
smfpimcclem.z 𝑍𝑉
smfpimcclem.s ( 𝜑𝑆𝑊 )
smfpimcclem.c ( ( 𝜑𝑦 ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) → ( 𝐶𝑦 ) ∈ 𝑦 )
smfpimcclem.h 𝐻 = ( 𝑛𝑍 ↦ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
Assertion smfpimcclem ( 𝜑 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 smfpimcclem.n 𝑛 𝜑
2 smfpimcclem.z 𝑍𝑉
3 smfpimcclem.s ( 𝜑𝑆𝑊 )
4 smfpimcclem.c ( ( 𝜑𝑦 ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) → ( 𝐶𝑦 ) ∈ 𝑦 )
5 smfpimcclem.h 𝐻 = ( 𝑛𝑍 ↦ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
6 nfcv 𝑠 𝑆
7 6 ssrab2f { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ⊆ 𝑆
8 eqid { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) }
9 8 3 rabexd ( 𝜑 → { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ V )
10 9 adantr ( ( 𝜑𝑛𝑍 ) → { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ V )
11 simpl ( ( 𝜑𝑛𝑍 ) → 𝜑 )
12 simpr ( ( 𝜑𝑛𝑍 ) → 𝑛𝑍 )
13 eqid ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) = ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } )
14 13 elrnmpt1 ( ( 𝑛𝑍 ∧ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ V ) → { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
15 12 10 14 syl2anc ( ( 𝜑𝑛𝑍 ) → { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
16 11 15 jca ( ( 𝜑𝑛𝑍 ) → ( 𝜑 ∧ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) )
17 eleq1 ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → ( 𝑦 ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ↔ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) )
18 17 anbi2d ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → ( ( 𝜑𝑦 ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) ↔ ( 𝜑 ∧ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) ) )
19 fveq2 ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → ( 𝐶𝑦 ) = ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
20 id ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } )
21 19 20 eleq12d ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → ( ( 𝐶𝑦 ) ∈ 𝑦 ↔ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
22 18 21 imbi12d ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } → ( ( ( 𝜑𝑦 ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) → ( 𝐶𝑦 ) ∈ 𝑦 ) ↔ ( ( 𝜑 ∧ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) → ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) )
23 22 4 vtoclg ( { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ V → ( ( 𝜑 ∧ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ∈ ran ( 𝑛𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) → ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
24 10 16 23 sylc ( ( 𝜑𝑛𝑍 ) → ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } )
25 7 24 sselid ( ( 𝜑𝑛𝑍 ) → ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ 𝑆 )
26 1 25 5 fmptdf ( 𝜑𝐻 : 𝑍𝑆 )
27 nfcv 𝑠 𝐶
28 nfrab1 𝑠 { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) }
29 27 28 nffv 𝑠 ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } )
30 nfcv 𝑠 ( ( 𝐹𝑛 ) “ 𝐴 )
31 nfcv 𝑠 dom ( 𝐹𝑛 )
32 29 31 nfin 𝑠 ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) )
33 30 32 nfeq 𝑠 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) )
34 ineq1 ( 𝑠 = ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) → ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) )
35 34 eqeq2d ( 𝑠 = ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) → ( ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) ↔ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) ) )
36 29 6 33 35 elrabf ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ↔ ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ 𝑆 ∧ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) ) )
37 24 36 sylib ( ( 𝜑𝑛𝑍 ) → ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ 𝑆 ∧ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) ) )
38 37 simprd ( ( 𝜑𝑛𝑍 ) → ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) )
39 5 a1i ( 𝜑𝐻 = ( 𝑛𝑍 ↦ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) )
40 24 elexd ( ( 𝜑𝑛𝑍 ) → ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∈ V )
41 39 40 fvmpt2d ( ( 𝜑𝑛𝑍 ) → ( 𝐻𝑛 ) = ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
42 41 ineq1d ( ( 𝜑𝑛𝑍 ) → ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) = ( ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ∩ dom ( 𝐹𝑛 ) ) )
43 38 42 eqtr4d ( ( 𝜑𝑛𝑍 ) → ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) )
44 43 ex ( 𝜑 → ( 𝑛𝑍 → ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
45 1 44 ralrimi ( 𝜑 → ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) )
46 2 elexi 𝑍 ∈ V
47 46 mptex ( 𝑛𝑍 ↦ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) ) ∈ V
48 5 47 eqeltri 𝐻 ∈ V
49 feq1 ( = 𝐻 → ( : 𝑍𝑆𝐻 : 𝑍𝑆 ) )
50 nfcv 𝑛
51 nfmpt1 𝑛 ( 𝑛𝑍 ↦ ( 𝐶 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑛 ) ) } ) )
52 5 51 nfcxfr 𝑛 𝐻
53 50 52 nfeq 𝑛 = 𝐻
54 fveq1 ( = 𝐻 → ( 𝑛 ) = ( 𝐻𝑛 ) )
55 54 ineq1d ( = 𝐻 → ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) )
56 55 eqeq2d ( = 𝐻 → ( ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ↔ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
57 53 56 ralbid ( = 𝐻 → ( ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ↔ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
58 49 57 anbi12d ( = 𝐻 → ( ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) ↔ ( 𝐻 : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) ) )
59 48 58 spcev ( ( 𝐻 : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝐻𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
60 26 45 59 syl2anc ( 𝜑 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )