Metamath Proof Explorer

Theorem fin23lem32

Description: Lemma for fin23 . Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
fin23lem17.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
fin23lem.b ⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
fin23lem.c ⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
fin23lem.d ⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
fin23lem.e ⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
Assertion fin23lem32 ( 𝐺 ∈ 𝐹 → ∃ 𝑓 ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2 fin23lem17.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3 fin23lem.b ⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
4 fin23lem.c ⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
5 fin23lem.d ⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
6 fin23lem.e ⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
7 1 2 3 4 5 6 fin23lem28 ⊢ ( 𝑡 : ω –1-1→ V → 𝑍 : ω –1-1→ V )
8 7 ad2antrl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑍 : ω –1-1→ V )
9 simprl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑡 : ω –1-1→ V )
10 simpl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝐺 ∈ 𝐹 )
11 simprr ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ∪ ran 𝑡 ⊆ 𝐺 )
12 1 2 3 4 5 6 fin23lem31 ⊢ ( ( 𝑡 : ω –1-1→ V ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )
13 9 10 11 12 syl3anc ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )
14 f1fn ⊢ ( 𝑡 : ω –1-1→ V → 𝑡 Fn ω )
15 dffn3 ⊢ ( 𝑡 Fn ω ↔ 𝑡 : ω ⟶ ran 𝑡 )
16 14 15 sylib ⊢ ( 𝑡 : ω –1-1→ V → 𝑡 : ω ⟶ ran 𝑡 )
17 16 ad2antrl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑡 : ω ⟶ ran 𝑡 )
18 sspwuni ⊢ ( ran 𝑡 ⊆ 𝒫 𝐺 ↔ ∪ ran 𝑡 ⊆ 𝐺 )
19 18 biimpri ⊢ ( ∪ ran 𝑡 ⊆ 𝐺 → ran 𝑡 ⊆ 𝒫 𝐺 )
20 19 ad2antll ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ran 𝑡 ⊆ 𝒫 𝐺 )
21 17 20 fssd ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑡 : ω ⟶ 𝒫 𝐺 )
22 pwexg ⊢ ( 𝐺 ∈ 𝐹 → 𝒫 𝐺 ∈ V )
23 22 adantr ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝒫 𝐺 ∈ V )
24 vex ⊢ 𝑡 ∈ V
25 f1f ⊢ ( 𝑡 : ω –1-1→ V → 𝑡 : ω ⟶ V )
26 dmfex ⊢ ( ( 𝑡 ∈ V ∧ 𝑡 : ω ⟶ V ) → ω ∈ V )
27 24 25 26 sylancr ⊢ ( 𝑡 : ω –1-1→ V → ω ∈ V )
28 27 ad2antrl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ω ∈ V )
29 23 28 elmapd ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↔ 𝑡 : ω ⟶ 𝒫 𝐺 ) )
30 21 29 mpbird ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) )
31 f1f ⊢ ( 𝑍 : ω –1-1→ V → 𝑍 : ω ⟶ V )
32 8 31 syl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑍 : ω ⟶ V )
33 32 28 fexd ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → 𝑍 ∈ V )
34 eqid ⊢ ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 )
35 34 fvmpt2 ⊢ ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ∧ 𝑍 ∈ V ) → ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 )
36 30 33 35 syl2anc ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 )
37 f1eq1 ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ↔ 𝑍 : ω –1-1→ V ) )
38 rneq ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 → ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = ran 𝑍 )
39 38 unieqd ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 → ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = ∪ ran 𝑍 )
40 39 psseq1d ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 → ( ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ↔ ∪ ran 𝑍 ⊊ ∪ ran 𝑡 ) )
41 37 40 anbi12d ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) = 𝑍 → ( ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ↔ ( 𝑍 : ω –1-1→ V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡 ) ) )
42 36 41 syl ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ( ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ↔ ( 𝑍 : ω –1-1→ V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡 ) ) )
43 8 13 42 mpbir2and ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) )
44 43 ex ⊢ ( 𝐺 ∈ 𝐹 → ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
45 44 alrimiv ⊢ ( 𝐺 ∈ 𝐹 → ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
46 ovex ⊢ ( 𝒫 𝐺 ↑m ω ) ∈ V
47 46 mptex ⊢ ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ∈ V
48 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 )
49 48 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 )
50 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( 𝑓 ‘ 𝑡 ) = ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) )
51 f1eq1 ⊢ ( ( 𝑓 ‘ 𝑡 ) = ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ↔ ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ) )
52 50 51 syl ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ↔ ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ) )
53 50 rneqd ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ran ( 𝑓 ‘ 𝑡 ) = ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) )
54 53 unieqd ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ∪ ran ( 𝑓 ‘ 𝑡 ) = ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) )
55 54 psseq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ↔ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) )
56 52 55 anbi12d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ↔ ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
57 56 imbi2d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) ↔ ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) ) )
58 49 57 albid ⊢ ( 𝑓 = ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) → ( ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) ↔ ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) ) )
59 47 58 spcev ⊢ ( ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( ( 𝑡 ∈ ( 𝒫 𝐺 ↑m ω ) ↦ 𝑍 ) ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) → ∃ 𝑓 ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
60 45 59 syl ⊢ ( 𝐺 ∈ 𝐹 → ∃ 𝑓 ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
61 f1eq1 ⊢ ( 𝑏 = 𝑡 → ( 𝑏 : ω –1-1→ V ↔ 𝑡 : ω –1-1→ V ) )
62 rneq ⊢ ( 𝑏 = 𝑡 → ran 𝑏 = ran 𝑡 )
63 62 unieqd ⊢ ( 𝑏 = 𝑡 → ∪ ran 𝑏 = ∪ ran 𝑡 )
64 63 sseq1d ⊢ ( 𝑏 = 𝑡 → ( ∪ ran 𝑏 ⊆ 𝐺 ↔ ∪ ran 𝑡 ⊆ 𝐺 ) )
65 61 64 anbi12d ⊢ ( 𝑏 = 𝑡 → ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) ↔ ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) )
66 fveq2 ⊢ ( 𝑏 = 𝑡 → ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑡 ) )
67 f1eq1 ⊢ ( ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑡 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ↔ ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ) )
68 66 67 syl ⊢ ( 𝑏 = 𝑡 → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ↔ ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ) )
69 66 rneqd ⊢ ( 𝑏 = 𝑡 → ran ( 𝑓 ‘ 𝑏 ) = ran ( 𝑓 ‘ 𝑡 ) )
70 69 unieqd ⊢ ( 𝑏 = 𝑡 → ∪ ran ( 𝑓 ‘ 𝑏 ) = ∪ ran ( 𝑓 ‘ 𝑡 ) )
71 70 63 psseq12d ⊢ ( 𝑏 = 𝑡 → ( ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ↔ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) )
72 68 71 anbi12d ⊢ ( 𝑏 = 𝑡 → ( ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ↔ ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
73 65 72 imbi12d ⊢ ( 𝑏 = 𝑡 → ( ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) ↔ ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) ) )
74 73 cbvalvw ⊢ ( ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) ↔ ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
75 74 exbii ⊢ ( ∃ 𝑓 ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) ↔ ∃ 𝑓 ∀ 𝑡 ( ( 𝑡 : ω –1-1→ V ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑡 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑡 ) ⊊ ∪ ran 𝑡 ) ) )
76 60 75 sylibr ⊢ ( 𝐺 ∈ 𝐹 → ∃ 𝑓 ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) )