Metamath Proof Explorer

Theorem fineqvlem

Description: Lemma for fineqv . (Contributed by Mario Carneiro, 20-Jan-2013) (Proof shortened by Stefan O'Rear, 3-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fineqvlem ⊢ A ∈ V ∧ ¬ A ∈ Fin → ω ≼ 𝒫 𝒫 A

Proof

Step Hyp Ref Expression
1 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
2 1 adantr ⊢ A ∈ V ∧ ¬ A ∈ Fin → 𝒫 A ∈ V
3 2 pwexd ⊢ A ∈ V ∧ ¬ A ∈ Fin → 𝒫 𝒫 A ∈ V
4 ssrab2 ⊢ d ∈ 𝒫 A | d ≈ b ⊆ 𝒫 A
5 elpw2g ⊢ 𝒫 A ∈ V → d ∈ 𝒫 A | d ≈ b ∈ 𝒫 𝒫 A ↔ d ∈ 𝒫 A | d ≈ b ⊆ 𝒫 A
6 2 5 syl ⊢ A ∈ V ∧ ¬ A ∈ Fin → d ∈ 𝒫 A | d ≈ b ∈ 𝒫 𝒫 A ↔ d ∈ 𝒫 A | d ≈ b ⊆ 𝒫 A
7 4 6 mpbiri ⊢ A ∈ V ∧ ¬ A ∈ Fin → d ∈ 𝒫 A | d ≈ b ∈ 𝒫 𝒫 A
8 7 a1d ⊢ A ∈ V ∧ ¬ A ∈ Fin → b ∈ ω → d ∈ 𝒫 A | d ≈ b ∈ 𝒫 𝒫 A
9 isinf ⊢ ¬ A ∈ Fin → ∀ b ∈ ω ∃ e e ⊆ A ∧ e ≈ b
10 9 r19.21bi ⊢ ¬ A ∈ Fin ∧ b ∈ ω → ∃ e e ⊆ A ∧ e ≈ b
11 10 ad2ant2lr ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω → ∃ e e ⊆ A ∧ e ≈ b
12 velpw ⊢ e ∈ 𝒫 A ↔ e ⊆ A
13 12 biimpri ⊢ e ⊆ A → e ∈ 𝒫 A
14 13 anim1i ⊢ e ⊆ A ∧ e ≈ b → e ∈ 𝒫 A ∧ e ≈ b
15 breq1 ⊢ d = e → d ≈ b ↔ e ≈ b
16 15 elrab ⊢ e ∈ d ∈ 𝒫 A | d ≈ b ↔ e ∈ 𝒫 A ∧ e ≈ b
17 14 16 sylibr ⊢ e ⊆ A ∧ e ≈ b → e ∈ d ∈ 𝒫 A | d ≈ b
18 17 eximi ⊢ ∃ e e ⊆ A ∧ e ≈ b → ∃ e e ∈ d ∈ 𝒫 A | d ≈ b
19 11 18 syl ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω → ∃ e e ∈ d ∈ 𝒫 A | d ≈ b
20 eleq2 ⊢ d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c → e ∈ d ∈ 𝒫 A | d ≈ b ↔ e ∈ d ∈ 𝒫 A | d ≈ c
21 20 biimpcd ⊢ e ∈ d ∈ 𝒫 A | d ≈ b → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c → e ∈ d ∈ 𝒫 A | d ≈ c
22 21 adantl ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω ∧ e ∈ d ∈ 𝒫 A | d ≈ b → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c → e ∈ d ∈ 𝒫 A | d ≈ c
23 16 simprbi ⊢ e ∈ d ∈ 𝒫 A | d ≈ b → e ≈ b
24 breq1 ⊢ d = e → d ≈ c ↔ e ≈ c
25 24 elrab ⊢ e ∈ d ∈ 𝒫 A | d ≈ c ↔ e ∈ 𝒫 A ∧ e ≈ c
26 25 simprbi ⊢ e ∈ d ∈ 𝒫 A | d ≈ c → e ≈ c
27 ensym ⊢ e ≈ b → b ≈ e
28 entr ⊢ b ≈ e ∧ e ≈ c → b ≈ c
29 27 28 sylan ⊢ e ≈ b ∧ e ≈ c → b ≈ c
30 23 26 29 syl2an ⊢ e ∈ d ∈ 𝒫 A | d ≈ b ∧ e ∈ d ∈ 𝒫 A | d ≈ c → b ≈ c
31 30 ex ⊢ e ∈ d ∈ 𝒫 A | d ≈ b → e ∈ d ∈ 𝒫 A | d ≈ c → b ≈ c
32 31 adantl ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω ∧ e ∈ d ∈ 𝒫 A | d ≈ b → e ∈ d ∈ 𝒫 A | d ≈ c → b ≈ c
33 nneneq ⊢ b ∈ ω ∧ c ∈ ω → b ≈ c ↔ b = c
34 33 biimpd ⊢ b ∈ ω ∧ c ∈ ω → b ≈ c → b = c
35 34 ad2antlr ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω ∧ e ∈ d ∈ 𝒫 A | d ≈ b → b ≈ c → b = c
36 22 32 35 3syld ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω ∧ e ∈ d ∈ 𝒫 A | d ≈ b → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c → b = c
37 19 36 exlimddv ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c → b = c
38 breq2 ⊢ b = c → d ≈ b ↔ d ≈ c
39 38 rabbidv ⊢ b = c → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c
40 37 39 impbid1 ⊢ A ∈ V ∧ ¬ A ∈ Fin ∧ b ∈ ω ∧ c ∈ ω → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c ↔ b = c
41 40 ex ⊢ A ∈ V ∧ ¬ A ∈ Fin → b ∈ ω ∧ c ∈ ω → d ∈ 𝒫 A | d ≈ b = d ∈ 𝒫 A | d ≈ c ↔ b = c
42 8 41 dom2d ⊢ A ∈ V ∧ ¬ A ∈ Fin → 𝒫 𝒫 A ∈ V → ω ≼ 𝒫 𝒫 A
43 3 42 mpd ⊢ A ∈ V ∧ ¬ A ∈ Fin → ω ≼ 𝒫 𝒫 A