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 )