This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ttukeylem6

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
ttukeylem.4 ⊢ 𝐺 = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
Assertion ttukeylem6 ( ( 𝜑 ∧ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
2 ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
4 ttukeylem.4 ⊢ 𝐺 = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
5 cardon ⊢ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On
6 5 onsuci ⊢ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On
7 6 a1i ⊢ ( 𝜑 → suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On )
8 onelon ⊢ ( ( suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → 𝐶 ∈ On )
9 7 8 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → 𝐶 ∈ On )
10 eleq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ↔ 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
11 fveq2 ⊢ ( 𝑦 = 𝑎 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑎 ) )
12 11 eleq1d ⊢ ( 𝑦 = 𝑎 → ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) )
13 10 12 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ↔ ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) )
14 13 imbi2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) ↔ ( 𝜑 → ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ) )
15 eleq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ↔ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝐶 ) )
17 16 eleq1d ⊢ ( 𝑦 = 𝐶 → ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 ) )
18 15 17 imbi12d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ↔ ( 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 ) ) )
19 18 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) ↔ ( 𝜑 → ( 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 ) ) ) )
20 r19.21v ⊢ ( ∀ 𝑎 ∈ 𝑦 ( 𝜑 → ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ↔ ( 𝜑 → ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) )
21 6 onordi ⊢ Ord suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) )
22 21 a1i ⊢ ( 𝜑 → Ord suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
23 ordelss ⊢ ( ( Ord suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → 𝑦 ⊆ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
24 22 23 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → 𝑦 ⊆ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
25 24 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑦 ) → 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
26 biimt ⊢ ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) )
27 25 26 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑦 ) → ( ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) )
28 27 ralbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ↔ ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) )
29 6 onssi ⊢ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ⊆ On
30 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
31 29 30 sselid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → 𝑦 ∈ On )
32 1 2 3 4 ttukeylem3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝐺 ‘ 𝑦 ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) )
33 31 32 syldan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑦 ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) )
34 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑦 = ∅ ) → 𝐵 ∈ 𝐴 )
35 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) )
36 35 elin2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ Fin )
37 35 elin1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ 𝒫 ∪ ( 𝐺 “ 𝑦 ) )
38 37 elpwid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ⊆ ∪ ( 𝐺 “ 𝑦 ) )
39 4 tfr1 ⊢ 𝐺 Fn On
40 fnfun ⊢ ( 𝐺 Fn On → Fun 𝐺 )
41 funiunfv ⊢ ( Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) = ∪ ( 𝐺 “ 𝑦 ) )
42 39 40 41 mp2b ⊢ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) = ∪ ( 𝐺 “ 𝑦 )
43 38 42 sseqtrrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) )
44 dfss3 ⊢ ( 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) ↔ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) )
45 eliun ⊢ ( 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝑦 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) )
46 45 ralbii ⊢ ( ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) ↔ ∀ 𝑢 ∈ 𝑤 ∃ 𝑣 ∈ 𝑦 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) )
47 44 46 bitri ⊢ ( 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 ( 𝐺 ‘ 𝑣 ) ↔ ∀ 𝑢 ∈ 𝑤 ∃ 𝑣 ∈ 𝑦 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) )
48 43 47 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → ∀ 𝑢 ∈ 𝑤 ∃ 𝑣 ∈ 𝑦 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) )
49 fveq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) )
50 49 eleq2d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) ↔ 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) )
51 50 ac6sfi ⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑢 ∈ 𝑤 ∃ 𝑣 ∈ 𝑦 𝑢 ∈ ( 𝐺 ‘ 𝑣 ) ) → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) )
52 36 48 51 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) )
53 eleq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
54 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝜑 )
55 fveq2 ⊢ ( 𝑎 = ∪ ran 𝑓 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ ∪ ran 𝑓 ) )
56 55 eleq1d ⊢ ( 𝑎 = ∪ ran 𝑓 → ( ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝐺 ‘ ∪ ran 𝑓 ) ∈ 𝐴 ) )
57 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 )
58 57 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 )
59 simprrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → 𝑓 : 𝑤 ⟶ 𝑦 )
60 59 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑓 : 𝑤 ⟶ 𝑦 )
61 frn ⊢ ( 𝑓 : 𝑤 ⟶ 𝑦 → ran 𝑓 ⊆ 𝑦 )
62 60 61 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ran 𝑓 ⊆ 𝑦 )
63 31 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑦 ∈ On )
64 onss ⊢ ( 𝑦 ∈ On → 𝑦 ⊆ On )
65 63 64 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑦 ⊆ On )
66 62 65 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ran 𝑓 ⊆ On )
67 36 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → 𝑤 ∈ Fin )
68 67 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑤 ∈ Fin )
69 ffn ⊢ ( 𝑓 : 𝑤 ⟶ 𝑦 → 𝑓 Fn 𝑤 )
70 60 69 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑓 Fn 𝑤 )
71 dffn4 ⊢ ( 𝑓 Fn 𝑤 ↔ 𝑓 : 𝑤 –onto→ ran 𝑓 )
72 70 71 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑓 : 𝑤 –onto→ ran 𝑓 )
73 fofi ⊢ ( ( 𝑤 ∈ Fin ∧ 𝑓 : 𝑤 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
74 68 72 73 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ran 𝑓 ∈ Fin )
75 dm0rn0 ⊢ ( dom 𝑓 = ∅ ↔ ran 𝑓 = ∅ )
76 59 fdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → dom 𝑓 = 𝑤 )
77 76 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → ( dom 𝑓 = ∅ ↔ 𝑤 = ∅ ) )
78 75 77 bitr3id ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → ( ran 𝑓 = ∅ ↔ 𝑤 = ∅ ) )
79 78 necon3bid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → ( ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅ ) )
80 79 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ran 𝑓 ≠ ∅ )
81 ordunifi ⊢ ( ( ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅ ) → ∪ ran 𝑓 ∈ ran 𝑓 )
82 66 74 80 81 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ∪ ran 𝑓 ∈ ran 𝑓 )
83 62 82 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ∪ ran 𝑓 ∈ 𝑦 )
84 56 58 83 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ( 𝐺 ‘ ∪ ran 𝑓 ) ∈ 𝐴 )
85 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → 𝜑 )
86 31 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → 𝑦 ∈ On )
87 86 64 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → 𝑦 ⊆ On )
88 ffvelcdm ⊢ ( ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) → ( 𝑓 ‘ 𝑢 ) ∈ 𝑦 )
89 88 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝑓 ‘ 𝑢 ) ∈ 𝑦 )
90 87 89 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝑓 ‘ 𝑢 ) ∈ On )
91 61 ad2antrl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ran 𝑓 ⊆ 𝑦 )
92 91 87 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ran 𝑓 ⊆ On )
93 vex ⊢ 𝑓 ∈ V
94 93 rnex ⊢ ran 𝑓 ∈ V
95 94 ssonunii ⊢ ( ran 𝑓 ⊆ On → ∪ ran 𝑓 ∈ On )
96 92 95 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ∪ ran 𝑓 ∈ On )
97 69 ad2antrl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → 𝑓 Fn 𝑤 )
98 simprr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → 𝑢 ∈ 𝑤 )
99 fnfvelrn ⊢ ( ( 𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤 ) → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 )
100 97 98 99 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 )
101 elssuni ⊢ ( ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 → ( 𝑓 ‘ 𝑢 ) ⊆ ∪ ran 𝑓 )
102 100 101 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝑓 ‘ 𝑢 ) ⊆ ∪ ran 𝑓 )
103 1 2 3 4 ttukeylem5 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ‘ 𝑢 ) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ ( 𝑓 ‘ 𝑢 ) ⊆ ∪ ran 𝑓 ) ) → ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ⊆ ( 𝐺 ‘ ∪ ran 𝑓 ) )
104 85 90 96 102 103 syl13anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ⊆ ( 𝐺 ‘ ∪ ran 𝑓 ) )
105 104 sseld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ 𝑢 ∈ 𝑤 ) ) → ( 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) → 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) ) )
106 105 anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ 𝑓 : 𝑤 ⟶ 𝑦 ) ∧ 𝑢 ∈ 𝑤 ) → ( 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) → 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) ) )
107 106 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) ∧ 𝑓 : 𝑤 ⟶ 𝑦 ) → ( ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) → ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) ) )
108 107 expimpd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → ( ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) → ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) ) )
109 108 impr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) )
110 109 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) )
111 dfss3 ⊢ ( 𝑤 ⊆ ( 𝐺 ‘ ∪ ran 𝑓 ) ↔ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ∪ ran 𝑓 ) )
112 110 111 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑤 ⊆ ( 𝐺 ‘ ∪ ran 𝑓 ) )
113 1 2 3 ttukeylem2 ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ∪ ran 𝑓 ) ∈ 𝐴 ∧ 𝑤 ⊆ ( 𝐺 ‘ ∪ ran 𝑓 ) ) ) → 𝑤 ∈ 𝐴 )
114 54 84 112 113 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) ∧ 𝑤 ≠ ∅ ) → 𝑤 ∈ 𝐴 )
115 0ss ⊢ ∅ ⊆ 𝐵
116 1 2 3 ttukeylem2 ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵 ) ) → ∅ ∈ 𝐴 )
117 115 116 mpanr2 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐴 ) → ∅ ∈ 𝐴 )
118 2 117 mpdan ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
119 118 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → ∅ ∈ 𝐴 )
120 53 114 119 pm2.61ne ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ∧ ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) ) ) → 𝑤 ∈ 𝐴 )
121 120 expr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → ( ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) → 𝑤 ∈ 𝐴 ) )
122 121 exlimdv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ∈ ( 𝐺 ‘ ( 𝑓 ‘ 𝑢 ) ) ) → 𝑤 ∈ 𝐴 ) )
123 52 122 mpd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ 𝐴 )
124 123 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ( 𝑤 ∈ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) → 𝑤 ∈ 𝐴 ) )
125 124 ssrdv ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ⊆ 𝐴 )
126 1 2 3 ttukeylem1 ⊢ ( 𝜑 → ( ∪ ( 𝐺 “ 𝑦 ) ∈ 𝐴 ↔ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ⊆ 𝐴 ) )
127 126 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ( ∪ ( 𝐺 “ 𝑦 ) ∈ 𝐴 ↔ ( 𝒫 ∪ ( 𝐺 “ 𝑦 ) ∩ Fin ) ⊆ 𝐴 ) )
128 125 127 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ∪ ( 𝐺 “ 𝑦 ) ∈ 𝐴 )
129 128 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) ∧ ¬ 𝑦 = ∅ ) → ∪ ( 𝐺 “ 𝑦 ) ∈ 𝐴 )
130 34 129 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ 𝑦 = ∪ 𝑦 ) → if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) ∈ 𝐴 )
131 uneq2 ⊢ ( { ( 𝐹 ‘ ∪ 𝑦 ) } = if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) → ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) = ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) )
132 131 eleq1d ⊢ ( { ( 𝐹 ‘ ∪ 𝑦 ) } = if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) → ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 ↔ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ∈ 𝐴 ) )
133 un0 ⊢ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ ∅ ) = ( 𝐺 ‘ ∪ 𝑦 )
134 uneq2 ⊢ ( ∅ = if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) → ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ ∅ ) = ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) )
135 133 134 eqtr3id ⊢ ( ∅ = if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) → ( 𝐺 ‘ ∪ 𝑦 ) = ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) )
136 135 eleq1d ⊢ ( ∅ = if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) → ( ( 𝐺 ‘ ∪ 𝑦 ) ∈ 𝐴 ↔ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ∈ 𝐴 ) )
137 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) ∧ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 ) → ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 )
138 fveq2 ⊢ ( 𝑎 = ∪ 𝑦 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ ∪ 𝑦 ) )
139 138 eleq1d ⊢ ( 𝑎 = ∪ 𝑦 → ( ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝐺 ‘ ∪ 𝑦 ) ∈ 𝐴 ) )
140 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 )
141 vuniex ⊢ ∪ 𝑦 ∈ V
142 141 sucid ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
144 orduniorsuc ⊢ ( Ord 𝑦 → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
145 31 143 144 3syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
146 145 orcanai ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → 𝑦 = suc ∪ 𝑦 )
147 142 146 eleqtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
148 139 140 147 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝐺 ‘ ∪ 𝑦 ) ∈ 𝐴 )
149 148 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) ∧ ¬ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 ) → ( 𝐺 ‘ ∪ 𝑦 ) ∈ 𝐴 )
150 132 136 137 149 ifbothda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ∈ 𝐴 )
151 130 150 ifclda ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) ∈ 𝐴 )
152 33 151 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 )
153 152 expr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) )
154 28 153 sylbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) )
155 154 ex ⊢ ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) )
156 155 com23 ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) )
157 156 a2i ⊢ ( ( 𝜑 → ∀ 𝑎 ∈ 𝑦 ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) )
158 20 157 sylbi ⊢ ( ∀ 𝑎 ∈ 𝑦 ( 𝜑 → ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) )
159 158 a1i ⊢ ( 𝑦 ∈ On → ( ∀ 𝑎 ∈ 𝑦 ( 𝜑 → ( 𝑎 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐴 ) ) → ( 𝜑 → ( 𝑦 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ) ) ) )
160 14 19 159 tfis3 ⊢ ( 𝐶 ∈ On → ( 𝜑 → ( 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 ) ) )
161 160 impd ⊢ ( 𝐶 ∈ On → ( ( 𝜑 ∧ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 ) )
162 9 161 mpcom ⊢ ( ( 𝜑 ∧ 𝐶 ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝐴 )