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

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 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
Assertion ttukeylem1 ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
2 ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
4 elex ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ V )
5 4 a1i ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ V ) )
6 id ⊢ ( ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 → ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 )
7 ssun1 ⊢ ∪ 𝐴 ⊆ ( ∪ 𝐴 ∪ 𝐵 )
8 undif1 ⊢ ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( ∪ 𝐴 ∪ 𝐵 )
9 7 8 sseqtrri ⊢ ∪ 𝐴 ⊆ ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 )
10 fvex ⊢ ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ V
11 f1ofo ⊢ ( 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
12 1 11 syl ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
13 focdmex ⊢ ( ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) ∈ V → ( 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –onto→ ( ∪ 𝐴 ∖ 𝐵 ) → ( ∪ 𝐴 ∖ 𝐵 ) ∈ V ) )
14 10 12 13 mpsyl ⊢ ( 𝜑 → ( ∪ 𝐴 ∖ 𝐵 ) ∈ V )
15 unexg ⊢ ( ( ( ∪ 𝐴 ∖ 𝐵 ) ∈ V ∧ 𝐵 ∈ 𝐴 ) → ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∈ V )
16 14 2 15 syl2anc ⊢ ( 𝜑 → ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∈ V )
17 ssexg ⊢ ( ( ∪ 𝐴 ⊆ ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∧ ( ( ∪ 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∈ V ) → ∪ 𝐴 ∈ V )
18 9 16 17 sylancr ⊢ ( 𝜑 → ∪ 𝐴 ∈ V )
19 uniexb ⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
20 18 19 sylibr ⊢ ( 𝜑 → 𝐴 ∈ V )
21 ssexg ⊢ ( ( ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ∧ 𝐴 ∈ V ) → ( 𝒫 𝐶 ∩ Fin ) ∈ V )
22 6 20 21 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) → ( 𝒫 𝐶 ∩ Fin ) ∈ V )
23 infpwfidom ⊢ ( ( 𝒫 𝐶 ∩ Fin ) ∈ V → 𝐶 ≼ ( 𝒫 𝐶 ∩ Fin ) )
24 reldom ⊢ Rel ≼
25 24 brrelex1i ⊢ ( 𝐶 ≼ ( 𝒫 𝐶 ∩ Fin ) → 𝐶 ∈ V )
26 22 23 25 3syl ⊢ ( ( 𝜑 ∧ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) → 𝐶 ∈ V )
27 26 ex ⊢ ( 𝜑 → ( ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 → 𝐶 ∈ V ) )
28 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
29 pweq ⊢ ( 𝑥 = 𝐶 → 𝒫 𝑥 = 𝒫 𝐶 )
30 29 ineq1d ⊢ ( 𝑥 = 𝐶 → ( 𝒫 𝑥 ∩ Fin ) = ( 𝒫 𝐶 ∩ Fin ) )
31 30 sseq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) )
32 28 31 bibi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ↔ ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) ) )
33 32 spcgv ⊢ ( 𝐶 ∈ V → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) ) )
34 3 33 syl5com ⊢ ( 𝜑 → ( 𝐶 ∈ V → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) ) )
35 5 27 34 pm5.21ndd ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝐴 ) )