Metamath Proof Explorer

Theorem ttukey2g

Description: The Teichmüller-Tukey Lemma ttukey with a slightly stronger conclusion: we can set up the maximal element of A so that it also contains some given B e. A as a subset. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion ttukey2g ( ( ∪ 𝐴 ∈ dom card ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 difss ⊢ ( ∪ 𝐴 ∖ 𝐵 ) ⊆ ∪ 𝐴
2 ssnum ⊢ ( ( ∪ 𝐴 ∈ dom card ∧ ( ∪ 𝐴 ∖ 𝐵 ) ⊆ ∪ 𝐴 ) → ( ∪ 𝐴 ∖ 𝐵 ) ∈ dom card )
3 1 2 mpan2 ⊢ ( ∪ 𝐴 ∈ dom card → ( ∪ 𝐴 ∖ 𝐵 ) ∈ dom card )
4 isnum3 ⊢ ( ( ∪ 𝐴 ∖ 𝐵 ) ∈ dom card ↔ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ≈ ( ∪ 𝐴 ∖ 𝐵 ) )
5 bren ⊢ ( ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ≈ ( ∪ 𝐴 ∖ 𝐵 ) ↔ ∃ 𝑓 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
6 4 5 bitri ⊢ ( ( ∪ 𝐴 ∖ 𝐵 ) ∈ dom card ↔ ∃ 𝑓 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
7 simp1 ⊢ ( ( 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
8 simp2 ⊢ ( ( 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
9 simp3 ⊢ ( ( 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
10 dmeq ⊢ ( 𝑤 = 𝑧 → dom 𝑤 = dom 𝑧 )
11 10 unieqd ⊢ ( 𝑤 = 𝑧 → ∪ dom 𝑤 = ∪ dom 𝑧 )
12 10 11 eqeq12d ⊢ ( 𝑤 = 𝑧 → ( dom 𝑤 = ∪ dom 𝑤 ↔ dom 𝑧 = ∪ dom 𝑧 ) )
13 10 eqeq1d ⊢ ( 𝑤 = 𝑧 → ( dom 𝑤 = ∅ ↔ dom 𝑧 = ∅ ) )
14 rneq ⊢ ( 𝑤 = 𝑧 → ran 𝑤 = ran 𝑧 )
15 14 unieqd ⊢ ( 𝑤 = 𝑧 → ∪ ran 𝑤 = ∪ ran 𝑧 )
16 13 15 ifbieq2d ⊢ ( 𝑤 = 𝑧 → if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) = if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) )
17 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
18 17 11 fveq12d ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ‘ ∪ dom 𝑤 ) = ( 𝑧 ‘ ∪ dom 𝑧 ) )
19 11 fveq2d ⊢ ( 𝑤 = 𝑧 → ( 𝑓 ‘ ∪ dom 𝑤 ) = ( 𝑓 ‘ ∪ dom 𝑧 ) )
20 19 sneqd ⊢ ( 𝑤 = 𝑧 → { ( 𝑓 ‘ ∪ dom 𝑤 ) } = { ( 𝑓 ‘ ∪ dom 𝑧 ) } )
21 18 20 uneq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) = ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) )
22 21 eleq1d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 ↔ ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 ) )
23 22 20 ifbieq1d ⊢ ( 𝑤 = 𝑧 → if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) = if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) )
24 18 23 uneq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) = ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) )
25 12 16 24 ifbieq12d ⊢ ( 𝑤 = 𝑧 → if ( dom 𝑤 = ∪ dom 𝑤 , if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) , ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) ) = if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) )
26 25 cbvmptv ⊢ ( 𝑤 ∈ V ↦ if ( dom 𝑤 = ∪ dom 𝑤 , if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) , ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) ) ) = ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) )
27 recseq ⊢ ( ( 𝑤 ∈ V ↦ if ( dom 𝑤 = ∪ dom 𝑤 , if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) , ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) ) ) = ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) → recs ( ( 𝑤 ∈ V ↦ if ( dom 𝑤 = ∪ dom 𝑤 , if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) , ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) ) ) ) = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) ) )
28 26 27 ax-mp ⊢ recs ( ( 𝑤 ∈ V ↦ if ( dom 𝑤 = ∪ dom 𝑤 , if ( dom 𝑤 = ∅ , 𝐵 , ∪ ran 𝑤 ) , ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ if ( ( ( 𝑤 ‘ ∪ dom 𝑤 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑤 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑤 ) } , ∅ ) ) ) ) ) = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝑓 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝑓 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
29 7 8 9 28 ttukeylem7 ⊢ ( ( 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )
30 29 3expib ⊢ ( 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) → ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
31 30 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) → ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
32 6 31 sylbi ⊢ ( ( ∪ 𝐴 ∖ 𝐵 ) ∈ dom card → ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
33 3 32 syl ⊢ ( ∪ 𝐴 ∈ dom card → ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
34 33 3impib ⊢ ( ( ∪ 𝐴 ∈ dom card ∧ 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )