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∈ω∃ee⊆A∧e≈b
10 9 r19.21bi ⊢¬A∈Fin∧b∈ω→∃ee⊆A∧e≈b
11 10 ad2ant2lr ⊢A∈V∧¬A∈Fin∧b∈ω∧c∈ω→∃ee⊆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 ⊢∃ee⊆A∧e≈b→∃ee∈d∈𝒫A|d≈b
19 11 18 syl ⊢A∈V∧¬A∈Fin∧b∈ω∧c∈ω→∃ee∈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