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

Metamath Proof Explorer

Theorem ttukeylem5

Description: Lemma for ttukey . The G function forms a (transfinitely long) chain of inclusions. (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 ttukeylem5 ( ( 𝜑 ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) )

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 sseq2 ⊢ ( 𝑦 = 𝑎 → ( 𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎 ) )
6 fveq2 ⊢ ( 𝑦 = 𝑎 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑎 ) )
7 6 sseq2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) )
8 5 7 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) )
9 8 imbi2d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) ) )
10 sseq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷 ) )
11 fveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝐷 ) )
12 11 sseq2d ⊢ ( 𝑦 = 𝐷 → ( ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) ) )
13 10 12 imbi12d ⊢ ( 𝑦 = 𝐷 → ( ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐶 ⊆ 𝐷 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) ) ) )
14 13 imbi2d ⊢ ( 𝑦 = 𝐷 → ( ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝐷 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) ) ) ) )
15 r19.21v ⊢ ( ∀ 𝑎 ∈ 𝑦 ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) ↔ ( ( 𝜑 ∧ 𝐶 ∈ On ) → ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) )
16 onsseleq ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 ⊆ 𝑦 ↔ ( 𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦 ) ) )
17 16 ad4ant23 ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( 𝐶 ⊆ 𝑦 ↔ ( 𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦 ) ) )
18 sseq2 ⊢ ( if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) → ( ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) ) )
19 sseq2 ⊢ ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) → ( ( 𝐺 ‘ 𝐶 ) ⊆ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ↔ ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) ) )
20 4 tfr1 ⊢ 𝐺 Fn On
21 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → 𝑦 ∈ On )
22 onss ⊢ ( 𝑦 ∈ On → 𝑦 ⊆ On )
23 21 22 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → 𝑦 ⊆ On )
24 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → 𝐶 ∈ 𝑦 )
25 fnfvima ⊢ ( ( 𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 “ 𝑦 ) )
26 20 23 24 25 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 “ 𝑦 ) )
27 elssuni ⊢ ( ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 “ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ ∪ ( 𝐺 “ 𝑦 ) )
28 26 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ ∪ ( 𝐺 “ 𝑦 ) )
29 n0i ⊢ ( 𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅ )
30 iffalse ⊢ ( ¬ 𝑦 = ∅ → if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) = ∪ ( 𝐺 “ 𝑦 ) )
31 24 29 30 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) = ∪ ( 𝐺 “ 𝑦 ) )
32 28 31 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) )
33 32 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ 𝑦 = ∪ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) )
34 24 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → 𝐶 ∈ 𝑦 )
35 elssuni ⊢ ( 𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦 )
36 34 35 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → 𝐶 ⊆ ∪ 𝑦 )
37 sseq2 ⊢ ( 𝑎 = ∪ 𝑦 → ( 𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦 ) )
38 fveq2 ⊢ ( 𝑎 = ∪ 𝑦 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ ∪ 𝑦 ) )
39 38 sseq2d ⊢ ( 𝑎 = ∪ 𝑦 → ( ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ↔ ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ ∪ 𝑦 ) ) )
40 37 39 imbi12d ⊢ ( 𝑎 = ∪ 𝑦 → ( ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ↔ ( 𝐶 ⊆ ∪ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ ∪ 𝑦 ) ) ) )
41 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) )
42 vuniex ⊢ ∪ 𝑦 ∈ V
43 42 sucid ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
44 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
45 orduniorsuc ⊢ ( Ord 𝑦 → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
46 21 44 45 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
47 46 orcanai ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → 𝑦 = suc ∪ 𝑦 )
48 43 47 eleqtrrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
49 40 41 48 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝐶 ⊆ ∪ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ ∪ 𝑦 ) ) )
50 36 49 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ ∪ 𝑦 ) )
51 ssun1 ⊢ ( 𝐺 ‘ ∪ 𝑦 ) ⊆ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) )
52 50 51 sstrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) ∧ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) )
53 18 19 33 52 ifbothda ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) )
54 1 2 3 4 ttukeylem3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝐺 ‘ 𝑦 ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) )
55 54 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝑦 ) = if ( 𝑦 = ∪ 𝑦 , if ( 𝑦 = ∅ , 𝐵 , ∪ ( 𝐺 “ 𝑦 ) ) , ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ if ( ( ( 𝐺 ‘ ∪ 𝑦 ) ∪ { ( 𝐹 ‘ ∪ 𝑦 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ 𝑦 ) } , ∅ ) ) ) )
56 53 55 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ∧ 𝐶 ∈ 𝑦 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) )
57 56 expr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( 𝐶 ∈ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) )
58 fveq2 ⊢ ( 𝐶 = 𝑦 → ( 𝐺 ‘ 𝐶 ) = ( 𝐺 ‘ 𝑦 ) )
59 eqimss ⊢ ( ( 𝐺 ‘ 𝐶 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) )
60 58 59 syl ⊢ ( 𝐶 = 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) )
61 60 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( 𝐶 = 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) )
62 57 61 jaod ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( ( 𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦 ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) )
63 17 62 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) ∧ ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) )
64 63 ex ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ On ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) )
65 64 expcom ⊢ ( 𝑦 ∈ On → ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) ) )
66 65 a2d ⊢ ( 𝑦 ∈ On → ( ( ( 𝜑 ∧ 𝐶 ∈ On ) → ∀ 𝑎 ∈ 𝑦 ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) ) )
67 15 66 biimtrid ⊢ ( 𝑦 ∈ On → ( ∀ 𝑎 ∈ 𝑦 ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑎 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑎 ) ) ) → ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝑦 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝑦 ) ) ) ) )
68 9 14 67 tfis3 ⊢ ( 𝐷 ∈ On → ( ( 𝜑 ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝐷 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) ) ) )
69 68 expdcom ⊢ ( 𝜑 → ( 𝐶 ∈ On → ( 𝐷 ∈ On → ( 𝐶 ⊆ 𝐷 → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) ) ) ) )
70 69 3imp2 ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐺 ‘ 𝐶 ) ⊆ ( 𝐺 ‘ 𝐷 ) )