Metamath Proof Explorer

Theorem ttukeylem1

Description: Lemma for ttukey . Expand out the property of being an element of a property of finite character. (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
Assertion ttukeylem1 ⊢ φ → C ∈ A ↔ 𝒫 C ∩ Fin ⊆ A

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 elex ⊢ C ∈ A → C ∈ V
5 4 a1i ⊢ φ → C ∈ A → C ∈ V
6 id ⊢ 𝒫 C ∩ Fin ⊆ A → 𝒫 C ∩ Fin ⊆ A
7 ssun1 ⊢ ⋃ A ⊆ ⋃ A ∪ B
8 undif1 ⊢ ⋃ A ∖ B ∪ B = ⋃ A ∪ B
9 7 8 sseqtrri ⊢ ⋃ A ⊆ ⋃ A ∖ B ∪ B
10 fvex ⊢ card ⁡ ⋃ A ∖ B ∈ V
11 f1ofo ⊢ F : card ⁡ ⋃ A ∖ B ⟶ 1-1 onto ⋃ A ∖ B → F : card ⁡ ⋃ A ∖ B ⟶ onto ⋃ A ∖ B
12 1 11 syl ⊢ φ → F : card ⁡ ⋃ A ∖ B ⟶ onto ⋃ A ∖ B
13 fornex ⊢ card ⁡ ⋃ A ∖ B ∈ V → F : card ⁡ ⋃ A ∖ B ⟶ onto ⋃ A ∖ B → ⋃ A ∖ B ∈ V
14 10 12 13 mpsyl ⊢ φ → ⋃ A ∖ B ∈ V
15 unexg ⊢ ⋃ A ∖ B ∈ V ∧ B ∈ A → ⋃ A ∖ B ∪ B ∈ V
16 14 2 15 syl2anc ⊢ φ → ⋃ A ∖ B ∪ B ∈ V
17 ssexg ⊢ ⋃ A ⊆ ⋃ A ∖ B ∪ B ∧ ⋃ A ∖ B ∪ B ∈ V → ⋃ A ∈ V
18 9 16 17 sylancr ⊢ φ → ⋃ A ∈ V
19 uniexb ⊢ A ∈ V ↔ ⋃ A ∈ V
20 18 19 sylibr ⊢ φ → A ∈ V
21 ssexg ⊢ 𝒫 C ∩ Fin ⊆ A ∧ A ∈ V → 𝒫 C ∩ Fin ∈ V
22 6 20 21 syl2anr ⊢ φ ∧ 𝒫 C ∩ Fin ⊆ A → 𝒫 C ∩ Fin ∈ V
23 infpwfidom ⊢ 𝒫 C ∩ Fin ∈ V → C ≼ 𝒫 C ∩ Fin
24 reldom ⊢ Rel ⁡ ≼
25 24 brrelex1i ⊢ C ≼ 𝒫 C ∩ Fin → C ∈ V
26 22 23 25 3syl ⊢ φ ∧ 𝒫 C ∩ Fin ⊆ A → C ∈ V
27 26 ex ⊢ φ → 𝒫 C ∩ Fin ⊆ A → C ∈ V
28 eleq1 ⊢ x = C → x ∈ A ↔ C ∈ A
29 pweq ⊢ x = C → 𝒫 x = 𝒫 C
30 29 ineq1d ⊢ x = C → 𝒫 x ∩ Fin = 𝒫 C ∩ Fin
31 30 sseq1d ⊢ x = C → 𝒫 x ∩ Fin ⊆ A ↔ 𝒫 C ∩ Fin ⊆ A
32 28 31 bibi12d ⊢ x = C → x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A ↔ C ∈ A ↔ 𝒫 C ∩ Fin ⊆ A
33 32 spcgv ⊢ C ∈ V → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → C ∈ A ↔ 𝒫 C ∩ Fin ⊆ A
34 3 33 syl5com ⊢ φ → C ∈ V → C ∈ A ↔ 𝒫 C ∩ Fin ⊆ A
35 5 27 34 pm5.21ndd ⊢ φ → C ∈ A ↔ 𝒫 C ∩ Fin ⊆ A