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

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 ( 𝐴 ∈ Fin → 𝐴 ∈ FinII )

Proof

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