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 ⊢ φ → F : card ⁡ ⋃ A ∖ B ⟶ 1-1 onto ⋃ A ∖ B
ttukeylem.2 ⊢ φ → B ∈ A
ttukeylem.3 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
Assertion ttukeylem5 ⊢ φ ∧ C ∈ On ∧ D ∈ On ∧ C ⊆ D → G ⁡ C ⊆ G ⁡ D

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ φ → F : card ⁡ ⋃ A ∖ B ⟶ 1-1 onto ⋃ A ∖ B
2 ttukeylem.2 ⊢ φ → B ∈ A
3 ttukeylem.3 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
4 ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
5 sseq2 ⊢ y = a → C ⊆ y ↔ C ⊆ a
6 fveq2 ⊢ y = a → G ⁡ y = G ⁡ a
7 6 sseq2d ⊢ y = a → G ⁡ C ⊆ G ⁡ y ↔ G ⁡ C ⊆ G ⁡ a
8 5 7 imbi12d ⊢ y = a → C ⊆ y → G ⁡ C ⊆ G ⁡ y ↔ C ⊆ a → G ⁡ C ⊆ G ⁡ a
9 8 imbi2d ⊢ y = a → φ ∧ C ∈ On → C ⊆ y → G ⁡ C ⊆ G ⁡ y ↔ φ ∧ C ∈ On → C ⊆ a → G ⁡ C ⊆ G ⁡ a
10 sseq2 ⊢ y = D → C ⊆ y ↔ C ⊆ D
11 fveq2 ⊢ y = D → G ⁡ y = G ⁡ D
12 11 sseq2d ⊢ y = D → G ⁡ C ⊆ G ⁡ y ↔ G ⁡ C ⊆ G ⁡ D
13 10 12 imbi12d ⊢ y = D → C ⊆ y → G ⁡ C ⊆ G ⁡ y ↔ C ⊆ D → G ⁡ C ⊆ G ⁡ D
14 13 imbi2d ⊢ y = D → φ ∧ C ∈ On → C ⊆ y → G ⁡ C ⊆ G ⁡ y ↔ φ ∧ C ∈ On → C ⊆ D → G ⁡ C ⊆ G ⁡ D
15 r19.21v ⊢ ∀ a ∈ y φ ∧ C ∈ On → C ⊆ a → G ⁡ C ⊆ G ⁡ a ↔ φ ∧ C ∈ On → ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a
16 onsseleq ⊢ C ∈ On ∧ y ∈ On → C ⊆ y ↔ C ∈ y ∨ C = y
17 16 ad4ant23 ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ⊆ y ↔ C ∈ y ∨ C = y
18 sseq2 ⊢ if y = ∅ B ⋃ G y = if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅ → G ⁡ C ⊆ if y = ∅ B ⋃ G y ↔ G ⁡ C ⊆ if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
19 sseq2 ⊢ G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅ = if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅ → G ⁡ C ⊆ G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅ ↔ G ⁡ C ⊆ if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
20 4 tfr1 ⊢ G Fn On
21 simplr ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → y ∈ On
22 onss ⊢ y ∈ On → y ⊆ On
23 21 22 syl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → y ⊆ On
24 simprr ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → C ∈ y
25 fnfvima ⊢ G Fn On ∧ y ⊆ On ∧ C ∈ y → G ⁡ C ∈ G y
26 20 23 24 25 mp3an2i ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ C ∈ G y
27 elssuni ⊢ G ⁡ C ∈ G y → G ⁡ C ⊆ ⋃ G y
28 26 27 syl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ C ⊆ ⋃ G y
29 n0i ⊢ C ∈ y → ¬ y = ∅
30 iffalse ⊢ ¬ y = ∅ → if y = ∅ B ⋃ G y = ⋃ G y
31 24 29 30 3syl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → if y = ∅ B ⋃ G y = ⋃ G y
32 28 31 sseqtrrd ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ C ⊆ if y = ∅ B ⋃ G y
33 32 adantr ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ y = ⋃ y → G ⁡ C ⊆ if y = ∅ B ⋃ G y
34 24 adantr ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → C ∈ y
35 elssuni ⊢ C ∈ y → C ⊆ ⋃ y
36 34 35 syl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → C ⊆ ⋃ y
37 sseq2 ⊢ a = ⋃ y → C ⊆ a ↔ C ⊆ ⋃ y
38 fveq2 ⊢ a = ⋃ y → G ⁡ a = G ⁡ ⋃ y
39 38 sseq2d ⊢ a = ⋃ y → G ⁡ C ⊆ G ⁡ a ↔ G ⁡ C ⊆ G ⁡ ⋃ y
40 37 39 imbi12d ⊢ a = ⋃ y → C ⊆ a → G ⁡ C ⊆ G ⁡ a ↔ C ⊆ ⋃ y → G ⁡ C ⊆ G ⁡ ⋃ y
41 simplrl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a
42 vuniex ⊢ ⋃ y ∈ V
43 42 sucid ⊢ ⋃ y ∈ suc ⁡ ⋃ y
44 eloni ⊢ y ∈ On → Ord ⁡ y
45 orduniorsuc ⊢ Ord ⁡ y → y = ⋃ y ∨ y = suc ⁡ ⋃ y
46 21 44 45 3syl ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → y = ⋃ y ∨ y = suc ⁡ ⋃ y
47 46 orcanai ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → y = suc ⁡ ⋃ y
48 43 47 eleqtrrid ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → ⋃ y ∈ y
49 40 41 48 rspcdva ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → C ⊆ ⋃ y → G ⁡ C ⊆ G ⁡ ⋃ y
50 36 49 mpd ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → G ⁡ C ⊆ G ⁡ ⋃ y
51 ssun1 ⊢ G ⁡ ⋃ y ⊆ G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
52 50 51 sstrdi ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y ∧ ¬ y = ⋃ y → G ⁡ C ⊆ G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
53 18 19 33 52 ifbothda ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ C ⊆ if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
54 1 2 3 4 ttukeylem3 ⊢ φ ∧ y ∈ On → G ⁡ y = if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
55 54 ad4ant13 ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ y = if y = ⋃ y if y = ∅ B ⋃ G y G ⁡ ⋃ y ∪ if G ⁡ ⋃ y ∪ F ⁡ ⋃ y ∈ A F ⁡ ⋃ y ∅
56 53 55 sseqtrrd ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a ∧ C ∈ y → G ⁡ C ⊆ G ⁡ y
57 56 expr ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ∈ y → G ⁡ C ⊆ G ⁡ y
58 fveq2 ⊢ C = y → G ⁡ C = G ⁡ y
59 eqimss ⊢ G ⁡ C = G ⁡ y → G ⁡ C ⊆ G ⁡ y
60 58 59 syl ⊢ C = y → G ⁡ C ⊆ G ⁡ y
61 60 a1i ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C = y → G ⁡ C ⊆ G ⁡ y
62 57 61 jaod ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ∈ y ∨ C = y → G ⁡ C ⊆ G ⁡ y
63 17 62 sylbid ⊢ φ ∧ C ∈ On ∧ y ∈ On ∧ ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ⊆ y → G ⁡ C ⊆ G ⁡ y
64 63 ex ⊢ φ ∧ C ∈ On ∧ y ∈ On → ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ⊆ y → G ⁡ C ⊆ G ⁡ y
65 64 expcom ⊢ y ∈ On → φ ∧ C ∈ On → ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → C ⊆ y → G ⁡ C ⊆ G ⁡ y
66 65 a2d ⊢ y ∈ On → φ ∧ C ∈ On → ∀ a ∈ y C ⊆ a → G ⁡ C ⊆ G ⁡ a → φ ∧ C ∈ On → C ⊆ y → G ⁡ C ⊆ G ⁡ y
67 15 66 biimtrid ⊢ y ∈ On → ∀ a ∈ y φ ∧ C ∈ On → C ⊆ a → G ⁡ C ⊆ G ⁡ a → φ ∧ C ∈ On → C ⊆ y → G ⁡ C ⊆ G ⁡ y
68 9 14 67 tfis3 ⊢ D ∈ On → φ ∧ C ∈ On → C ⊆ D → G ⁡ C ⊆ G ⁡ D
69 68 expdcom ⊢ φ → C ∈ On → D ∈ On → C ⊆ D → G ⁡ C ⊆ G ⁡ D
70 69 3imp2 ⊢ φ ∧ C ∈ On ∧ D ∈ On ∧ C ⊆ D → G ⁡ C ⊆ G ⁡ D