Theorem isfin2

Description: Definition of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	⊢ ( 𝑧 = 𝑥 → 𝒫 𝑧 = 𝒫 𝑥 )
2	1	pweqd	⊢ ( 𝑧 = 𝑥 → 𝒫 𝒫 𝑧 = 𝒫 𝒫 𝑥 )
3	2	raleqdv	⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝑧 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ) )
4		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
5	4	pweqd	⊢ ( 𝑥 = 𝐴 → 𝒫 𝒫 𝑥 = 𝒫 𝒫 𝐴 )
6	5	raleqdv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ) )
7		df-fin2	⊢ FinII = { 𝑧 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑧 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }
8	3 6 7	elab2gw	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ) )