Metamath Proof Explorer

Theorem ttukeylem7

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 ttukeylem7 ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )

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 fvex ⊢ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ V
6 5 sucid ⊢ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) )
7 1 2 3 4 ttukeylem6 ⊢ ( ( 𝜑 ∧ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ suc ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∈ 𝐴 )
8 6 7 mpan2 ⊢ ( 𝜑 → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∈ 𝐴 )
9 1 2 3 4 ttukeylem4 ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐵 )
10 0elon ⊢ ∅ ∈ On
11 cardon ⊢ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On
12 0ss ⊢ ∅ ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) )
13 10 11 12 3pm3.2i ⊢ ( ∅ ∈ On ∧ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ ∅ ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
14 1 2 3 4 ttukeylem5 ⊢ ( ( 𝜑 ∧ ( ∅ ∈ On ∧ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ ∅ ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ) → ( 𝐺 ‘ ∅ ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
15 13 14 mpan2 ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
16 9 15 eqsstrrd ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 )
18 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ 𝐵 )
19 undif1 ⊢ ( ( 𝑦 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝑦 ∪ 𝐵 )
20 18 19 sseqtrri ⊢ 𝑦 ⊆ ( ( 𝑦 ∖ 𝐵 ) ∪ 𝐵 )
21 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝜑 )
22 f1ocnv ⊢ ( 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) → ◡ 𝐹 : ( ∪ 𝐴 ∖ 𝐵 ) –1-1-onto→ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
23 f1of ⊢ ( ◡ 𝐹 : ( ∪ 𝐴 ∖ 𝐵 ) –1-1-onto→ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ◡ 𝐹 : ( ∪ 𝐴 ∖ 𝐵 ) ⟶ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
24 1 22 23 3syl ⊢ ( 𝜑 → ◡ 𝐹 : ( ∪ 𝐴 ∖ 𝐵 ) ⟶ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ◡ 𝐹 : ( ∪ 𝐴 ∖ 𝐵 ) ⟶ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
26 eldifi ⊢ ( 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) → 𝑎 ∈ 𝑦 )
27 26 ad2antll ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ 𝑦 )
28 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑦 ∈ 𝐴 )
29 elunii ⊢ ( ( 𝑎 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑎 ∈ ∪ 𝐴 )
30 27 28 29 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ ∪ 𝐴 )
31 eldifn ⊢ ( 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) → ¬ 𝑎 ∈ 𝐵 )
32 31 ad2antll ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ¬ 𝑎 ∈ 𝐵 )
33 30 32 eldifd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ ( ∪ 𝐴 ∖ 𝐵 ) )
34 25 33 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
35 onelon ⊢ ( ( ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ On )
36 11 34 35 sylancr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ On )
37 suceloni ⊢ ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ On → suc ( ◡ 𝐹 ‘ 𝑎 ) ∈ On )
38 36 37 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ∈ On )
39 11 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On )
40 11 onordi ⊢ Ord ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) )
41 ordsucss ⊢ ( Ord ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
42 40 34 41 mpsyl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
43 1 2 3 4 ttukeylem5 ⊢ ( ( 𝜑 ∧ ( suc ( ◡ 𝐹 ‘ 𝑎 ) ∈ On ∧ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ suc ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ) → ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
44 21 38 39 42 43 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
45 ssun2 ⊢ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ⊆ ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) )
46 eloni ⊢ ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ On → Ord ( ◡ 𝐹 ‘ 𝑎 ) )
47 ordunisuc ⊢ ( Ord ( ◡ 𝐹 ‘ 𝑎 ) → ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) = ( ◡ 𝐹 ‘ 𝑎 ) )
48 36 46 47 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) = ( ◡ 𝐹 ‘ 𝑎 ) )
49 48 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) )
50 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
51 f1ocnvfv2 ⊢ ( ( 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) ∧ 𝑎 ∈ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
52 50 33 51 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
53 49 52 eqtr2d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 = ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) )
54 velsn ⊢ ( 𝑎 ∈ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ↔ 𝑎 = ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) )
55 53 54 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } )
56 48 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) = ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) )
57 ordelss ⊢ ( ( Ord ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∧ ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
58 40 34 57 sylancr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) )
59 1 2 3 4 ttukeylem5 ⊢ ( ( 𝜑 ∧ ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ On ∧ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ On ∧ ( ◡ 𝐹 ‘ 𝑎 ) ⊆ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ) → ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
60 21 36 39 58 59 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
61 56 60 eqsstrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
62 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 )
63 61 62 sstrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ⊆ 𝑦 )
64 53 27 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∈ 𝑦 )
65 64 snssd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ⊆ 𝑦 )
66 63 65 unssd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ⊆ 𝑦 )
67 1 2 3 ttukeylem2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ⊆ 𝑦 ) ) → ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 )
68 21 28 66 67 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 )
69 68 iftrued ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) = { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } )
70 55 69 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) )
71 45 70 sseldi ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) )
72 1 2 3 4 ttukeylem3 ⊢ ( ( 𝜑 ∧ suc ( ◡ 𝐹 ‘ 𝑎 ) ∈ On ) → ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) = if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) , if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∅ , 𝐵 , ∪ ( 𝐺 “ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ) , ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) ) )
73 38 72 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) = if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) , if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∅ , 𝐵 , ∪ ( 𝐺 “ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ) , ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) ) )
74 sucidg ⊢ ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ suc ( ◡ 𝐹 ‘ 𝑎 ) )
75 34 74 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ suc ( ◡ 𝐹 ‘ 𝑎 ) )
76 ordirr ⊢ ( Ord ( ◡ 𝐹 ‘ 𝑎 ) → ¬ ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( ◡ 𝐹 ‘ 𝑎 ) )
77 36 46 76 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ¬ ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( ◡ 𝐹 ‘ 𝑎 ) )
78 nelne1 ⊢ ( ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ suc ( ◡ 𝐹 ‘ 𝑎 ) ∧ ¬ ( ◡ 𝐹 ‘ 𝑎 ) ∈ ( ◡ 𝐹 ‘ 𝑎 ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ≠ ( ◡ 𝐹 ‘ 𝑎 ) )
79 75 77 78 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ≠ ( ◡ 𝐹 ‘ 𝑎 ) )
80 79 48 neeqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → suc ( ◡ 𝐹 ‘ 𝑎 ) ≠ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) )
81 80 neneqd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ¬ suc ( ◡ 𝐹 ‘ 𝑎 ) = ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) )
82 81 iffalsed ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) , if ( suc ( ◡ 𝐹 ‘ 𝑎 ) = ∅ , 𝐵 , ∪ ( 𝐺 “ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ) , ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) ) = ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) )
83 73 82 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) = ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ if ( ( ( 𝐺 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) ∪ { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ suc ( ◡ 𝐹 ‘ 𝑎 ) ) } , ∅ ) ) )
84 71 83 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ ( 𝐺 ‘ suc ( ◡ 𝐹 ‘ 𝑎 ) ) )
85 44 84 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ∧ 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) ) ) → 𝑎 ∈ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
86 85 expr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → ( 𝑎 ∈ ( 𝑦 ∖ 𝐵 ) → 𝑎 ∈ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ) )
87 86 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → ( 𝑦 ∖ 𝐵 ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
88 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → 𝐵 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
89 87 88 unssd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → ( ( 𝑦 ∖ 𝐵 ) ∪ 𝐵 ) ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
90 20 89 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → 𝑦 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) )
91 17 90 eqssd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 ) ) → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) = 𝑦 )
92 91 expr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) = 𝑦 ) )
93 npss ⊢ ( ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ↔ ( ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊆ 𝑦 → ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) = 𝑦 ) )
94 92 93 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 )
95 94 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 )
96 sseq2 ⊢ ( 𝑥 = ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ) )
97 psseq1 ⊢ ( 𝑥 = ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( 𝑥 ⊊ 𝑦 ↔ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ) )
98 97 notbid ⊢ ( 𝑥 = ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ¬ 𝑥 ⊊ 𝑦 ↔ ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ) )
99 98 ralbidv ⊢ ( 𝑥 = ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ) )
100 96 99 anbi12d ⊢ ( 𝑥 = ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) → ( ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ↔ ( 𝐵 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ) ) )
101 100 rspcev ⊢ ( ( ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∈ 𝐴 ∧ ( 𝐵 ⊆ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐺 ‘ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ) ⊊ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )
102 8 16 95 101 syl12anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )