Metamath Proof Explorer

Theorem isfin7-2

Description: A set is VII-finite iff it is non-well-orderable or finite. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin7-2 ⊢ A ∈ V → A ∈ FinVII ↔ A ∈ dom ⁡ card → A ∈ Fin

Proof

Step Hyp Ref Expression
1 isfin7 ⊢ A ∈ FinVII → A ∈ FinVII ↔ ¬ ∃ x ∈ On ∖ ω A ≈ x
2 1 ibi ⊢ A ∈ FinVII → ¬ ∃ x ∈ On ∖ ω A ≈ x
3 isnum2 ⊢ A ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ A
4 ensym ⊢ x ≈ A → A ≈ x
5 simprl ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ A ≈ x → x ∈ On
6 enfi ⊢ A ≈ x → A ∈ Fin ↔ x ∈ Fin
7 onfin ⊢ x ∈ On → x ∈ Fin ↔ x ∈ ω
8 6 7 sylan9bbr ⊢ x ∈ On ∧ A ≈ x → A ∈ Fin ↔ x ∈ ω
9 8 biimprd ⊢ x ∈ On ∧ A ≈ x → x ∈ ω → A ∈ Fin
10 9 con3d ⊢ x ∈ On ∧ A ≈ x → ¬ A ∈ Fin → ¬ x ∈ ω
11 10 impcom ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ A ≈ x → ¬ x ∈ ω
12 5 11 eldifd ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ A ≈ x → x ∈ On ∖ ω
13 simprr ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ A ≈ x → A ≈ x
14 12 13 jca ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ A ≈ x → x ∈ On ∖ ω ∧ A ≈ x
15 4 14 sylanr2 ⊢ ¬ A ∈ Fin ∧ x ∈ On ∧ x ≈ A → x ∈ On ∖ ω ∧ A ≈ x
16 15 ex ⊢ ¬ A ∈ Fin → x ∈ On ∧ x ≈ A → x ∈ On ∖ ω ∧ A ≈ x
17 16 reximdv2 ⊢ ¬ A ∈ Fin → ∃ x ∈ On x ≈ A → ∃ x ∈ On ∖ ω A ≈ x
18 17 com12 ⊢ ∃ x ∈ On x ≈ A → ¬ A ∈ Fin → ∃ x ∈ On ∖ ω A ≈ x
19 3 18 sylbi ⊢ A ∈ dom ⁡ card → ¬ A ∈ Fin → ∃ x ∈ On ∖ ω A ≈ x
20 19 con1d ⊢ A ∈ dom ⁡ card → ¬ ∃ x ∈ On ∖ ω A ≈ x → A ∈ Fin
21 2 20 syl5com ⊢ A ∈ FinVII → A ∈ dom ⁡ card → A ∈ Fin
22 eldifi ⊢ x ∈ On ∖ ω → x ∈ On
23 ensym ⊢ A ≈ x → x ≈ A
24 isnumi ⊢ x ∈ On ∧ x ≈ A → A ∈ dom ⁡ card
25 22 23 24 syl2an ⊢ x ∈ On ∖ ω ∧ A ≈ x → A ∈ dom ⁡ card
26 25 rexlimiva ⊢ ∃ x ∈ On ∖ ω A ≈ x → A ∈ dom ⁡ card
27 26 con3i ⊢ ¬ A ∈ dom ⁡ card → ¬ ∃ x ∈ On ∖ ω A ≈ x
28 isfin7 ⊢ A ∈ V → A ∈ FinVII ↔ ¬ ∃ x ∈ On ∖ ω A ≈ x
29 27 28 syl5ibr ⊢ A ∈ V → ¬ A ∈ dom ⁡ card → A ∈ FinVII
30 fin17 ⊢ A ∈ Fin → A ∈ FinVII
31 30 a1i ⊢ A ∈ V → A ∈ Fin → A ∈ FinVII
32 29 31 jad ⊢ A ∈ V → A ∈ dom ⁡ card → A ∈ Fin → A ∈ FinVII
33 21 32 impbid2 ⊢ A ∈ V → A ∈ FinVII ↔ A ∈ dom ⁡ card → A ∈ Fin