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

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 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) )

Proof

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