Metamath Proof Explorer

Theorem smfpimcc

Description: Given a countable set of sigma-measurable functions, and a Borel set A there exists a choice function h that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of A . This is a generalization of the observation at the beginning of the proof of Proposition 121F of Fremlin1 p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfpimcc.1 ⊢ Ⅎ 𝑛 𝐹
smfpimcc.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smfpimcc.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfpimcc.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smfpimcc.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
smfpimcc.b ⊢ 𝐵 = ( SalGen ‘ 𝐽 )
smfpimcc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion smfpimcc ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 smfpimcc.1 ⊢ Ⅎ 𝑛 𝐹
2 smfpimcc.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smfpimcc.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smfpimcc.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smfpimcc.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
6 smfpimcc.b ⊢ 𝐵 = ( SalGen ‘ 𝐽 )
7 smfpimcc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8 2 uzct ⊢ 𝑍 ≼ ω
9 8 a1i ⊢ ( 𝜑 → 𝑍 ≼ ω )
10 mptct ⊢ ( 𝑍 ≼ ω → ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ≼ ω )
11 rnct ⊢ ( ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ≼ ω → ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ≼ ω )
12 9 10 11 3syl ⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ≼ ω )
13 vex ⊢ 𝑦 ∈ V
14 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) = ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
15 14 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ↔ ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
16 13 15 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ↔ ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
17 16 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
18 simp3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
20 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
21 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
22 7 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐴 ∈ 𝐵 )
23 eqid ⊢ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 )
24 19 20 21 5 6 22 23 smfpimbor1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) )
25 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
26 25 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
27 26 a1i ⊢ ( 𝜑 → dom ( 𝐹 ‘ 𝑚 ) ∈ V )
28 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
29 3 27 28 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
31 24 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
32 rabn0 ⊢ ( { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
33 31 32 sylibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
34 33 3adant3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
35 18 34 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 ≠ ∅ )
36 35 3exp ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 → ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) ) )
37 36 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
39 17 38 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → 𝑦 ≠ ∅ )
40 12 39 axccd2 ⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
41 nfv ⊢ Ⅎ 𝑚 𝜑
42 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
43 42 nfrn ⊢ Ⅎ 𝑚 ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
44 nfv ⊢ Ⅎ 𝑚 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦
45 43 44 nfralw ⊢ Ⅎ 𝑚 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦
46 41 45 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
47 2 fvexi ⊢ 𝑍 ∈ V
48 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑆 ∈ SAlg )
49 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑤 ) )
50 id ⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
51 49 50 eleq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
52 51 rspccva ⊢ ( ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ∧ 𝑤 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 )
53 52 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑤 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 )
54 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑓 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑓 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
55 46 47 48 53 54 smfpimcclem ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
56 55 ex ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) )
57 56 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) )
58 40 57 mpd ⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
59 nfcv ⊢ Ⅎ 𝑛 𝑚
60 1 59 nffv ⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑚 )
61 60 nfcnv ⊢ Ⅎ 𝑛 ◡ ( 𝐹 ‘ 𝑚 )
62 nfcv ⊢ Ⅎ 𝑛 𝐴
63 61 62 nfima ⊢ Ⅎ 𝑛 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 )
64 nfcv ⊢ Ⅎ 𝑛 ( ℎ ‘ 𝑚 )
65 60 nfdm ⊢ Ⅎ 𝑛 dom ( 𝐹 ‘ 𝑚 )
66 64 65 nfin ⊢ Ⅎ 𝑛 ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) )
67 63 66 nfeq ⊢ Ⅎ 𝑛 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) )
68 nfv ⊢ Ⅎ 𝑚 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) )
69 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
70 69 cnveqd ⊢ ( 𝑚 = 𝑛 → ◡ ( 𝐹 ‘ 𝑚 ) = ◡ ( 𝐹 ‘ 𝑛 ) )
71 70 imaeq1d ⊢ ( 𝑚 = 𝑛 → ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) )
72 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑛 ) )
73 69 dmeqd ⊢ ( 𝑚 = 𝑛 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑛 ) )
74 72 73 ineq12d ⊢ ( 𝑚 = 𝑛 → ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
75 71 74 eqeq12d ⊢ ( 𝑚 = 𝑛 → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
76 67 68 75 cbvralw ⊢ ( ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
77 76 anbi2i ⊢ ( ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ↔ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
78 77 exbii ⊢ ( ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ↔ ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
79 58 78 sylib ⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )