Metamath Proof Explorer

Theorem fin12

Description: Weak theorem which skips Ia but has a trivial proof, needed to prove fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin12 ⊢ A ∈ Fin → A ∈ FinII

Proof

Step Hyp Ref Expression
1 vex ⊢ b ∈ V
2 1 a1i ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → b ∈ V
3 isfin1-3 ⊢ A ∈ Fin → A ∈ Fin ↔ [⊂] -1 Fr 𝒫 A
4 3 ibi ⊢ A ∈ Fin → [⊂] -1 Fr 𝒫 A
5 4 ad2antrr ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → [⊂] -1 Fr 𝒫 A
6 elpwi ⊢ b ∈ 𝒫 𝒫 A → b ⊆ 𝒫 A
7 6 ad2antlr ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → b ⊆ 𝒫 A
8 simprl ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → b ≠ ∅
9 fri ⊢ b ∈ V ∧ [⊂] -1 Fr 𝒫 A ∧ b ⊆ 𝒫 A ∧ b ≠ ∅ → ∃ c ∈ b ∀ d ∈ b ¬ d [⊂] -1 c
10 2 5 7 8 9 syl22anc ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ c ∈ b ∀ d ∈ b ¬ d [⊂] -1 c
11 vex ⊢ d ∈ V
12 vex ⊢ c ∈ V
13 11 12 brcnv ⊢ d [⊂] -1 c ↔ c [⊂] d
14 11 brrpss ⊢ c [⊂] d ↔ c ⊂ d
15 13 14 bitri ⊢ d [⊂] -1 c ↔ c ⊂ d
16 15 notbii ⊢ ¬ d [⊂] -1 c ↔ ¬ c ⊂ d
17 16 ralbii ⊢ ∀ d ∈ b ¬ d [⊂] -1 c ↔ ∀ d ∈ b ¬ c ⊂ d
18 17 rexbii ⊢ ∃ c ∈ b ∀ d ∈ b ¬ d [⊂] -1 c ↔ ∃ c ∈ b ∀ d ∈ b ¬ c ⊂ d
19 10 18 sylib ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ c ∈ b ∀ d ∈ b ¬ c ⊂ d
20 sorpssuni ⊢ [⊂] Or b → ∃ c ∈ b ∀ d ∈ b ¬ c ⊂ d ↔ ⋃ b ∈ b
21 20 ad2antll ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ c ∈ b ∀ d ∈ b ¬ c ⊂ d ↔ ⋃ b ∈ b
22 19 21 mpbid ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A ∧ b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
23 22 ex ⊢ A ∈ Fin ∧ b ∈ 𝒫 𝒫 A → b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
24 23 ralrimiva ⊢ A ∈ Fin → ∀ b ∈ 𝒫 𝒫 A b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
25 isfin2 ⊢ A ∈ Fin → A ∈ FinII ↔ ∀ b ∈ 𝒫 𝒫 A b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
26 24 25 mpbird ⊢ A ∈ Fin → A ∈ FinII