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 syl5ibr ( 𝐴𝑉 → ( ¬ 𝐴 ∈ 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 ) ) )