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 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
19 simp3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
21 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
22 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐴 ∈ 𝐵 )
24 eqid ⊢ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 )
25 20 21 22 5 6 23 24 smfpimbor1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) )
26 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
27 26 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
28 27 a1i ⊢ ( 𝜑 → dom ( 𝐹 ‘ 𝑚 ) ∈ V )
29 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
30 3 28 29 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
32 25 31 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
33 rabn0 ⊢ ( { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ ↔ ∃ 𝑠 ∈ 𝑆 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
34 32 33 sylibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
35 34 3adant3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ≠ ∅ )
36 19 35 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) → 𝑦 ≠ ∅ )
37 36 3exp ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 → ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) ) )
38 37 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( ∃ 𝑚 ∈ 𝑍 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } → 𝑦 ≠ ∅ ) )
40 18 39 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → 𝑦 ≠ ∅ )
41 12 40 axccd2 ⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
42 nfv ⊢ Ⅎ 𝑚 𝜑
43 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
44 43 nfrn ⊢ Ⅎ 𝑚 ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
45 nfv ⊢ Ⅎ 𝑚 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦
46 44 45 nfralw ⊢ Ⅎ 𝑚 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦
47 42 46 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
48 2 fvexi ⊢ 𝑍 ∈ V
49 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → 𝑆 ∈ SAlg )
50 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑤 ) )
51 id ⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
52 50 51 eleq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
53 52 rspccva ⊢ ( ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ∧ 𝑤 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 )
54 53 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑤 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 )
55 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑓 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑓 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) )
56 47 48 49 54 55 smfpimcclem ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
57 56 ex ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) )
58 57 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ∀ 𝑦 ∈ ran ( 𝑚 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) )
59 41 58 mpd ⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
60 nfcv ⊢ Ⅎ 𝑛 𝑚
61 1 60 nffv ⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑚 )
62 61 nfcnv ⊢ Ⅎ 𝑛 ◡ ( 𝐹 ‘ 𝑚 )
63 nfcv ⊢ Ⅎ 𝑛 𝐴
64 62 63 nfima ⊢ Ⅎ 𝑛 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 )
65 nfcv ⊢ Ⅎ 𝑛 ( ℎ ‘ 𝑚 )
66 61 nfdm ⊢ Ⅎ 𝑛 dom ( 𝐹 ‘ 𝑚 )
67 65 66 nfin ⊢ Ⅎ 𝑛 ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) )
68 64 67 nfeq ⊢ Ⅎ 𝑛 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) )
69 nfv ⊢ Ⅎ 𝑚 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) )
70 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
71 70 cnveqd ⊢ ( 𝑚 = 𝑛 → ◡ ( 𝐹 ‘ 𝑚 ) = ◡ ( 𝐹 ‘ 𝑛 ) )
72 71 imaeq1d ⊢ ( 𝑚 = 𝑛 → ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) )
73 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑛 ) )
74 70 dmeqd ⊢ ( 𝑚 = 𝑛 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑛 ) )
75 73 74 ineq12d ⊢ ( 𝑚 = 𝑛 → ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
76 72 75 eqeq12d ⊢ ( 𝑚 = 𝑛 → ( ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
77 68 69 76 cbvralw ⊢ ( ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
78 77 anbi2i ⊢ ( ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ↔ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
79 78 exbii ⊢ ( ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑚 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑚 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ↔ ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
80 59 79 sylib ⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )