Theorem dffin7-2

Description: Class form of isfin7-2 . (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	dffin7-2	⊢ FinVII = ( Fin ∪ ( V ∖ dom card ) )

Proof

Step	Hyp	Ref	Expression
1		imor	⊢ ( ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
2		isfin7-2	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ FinVII ↔ ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) ) )
3	2	elv	⊢ ( 𝑥 ∈ FinVII ↔ ( 𝑥 ∈ dom card → 𝑥 ∈ Fin ) )
4		elun	⊢ ( 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) ↔ ( 𝑥 ∈ Fin ∨ 𝑥 ∈ ( V ∖ dom card ) ) )
5		orcom	⊢ ( ( 𝑥 ∈ Fin ∨ 𝑥 ∈ ( V ∖ dom card ) ) ↔ ( 𝑥 ∈ ( V ∖ dom card ) ∨ 𝑥 ∈ Fin ) )
6		vex	⊢ 𝑥 ∈ V
7		eldif	⊢ ( 𝑥 ∈ ( V ∖ dom card ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom card ) )
8	6 7	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ dom card ) ↔ ¬ 𝑥 ∈ dom card )
9	8	orbi1i	⊢ ( ( 𝑥 ∈ ( V ∖ dom card ) ∨ 𝑥 ∈ Fin ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
10	4 5 9	3bitri	⊢ ( 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) ↔ ( ¬ 𝑥 ∈ dom card ∨ 𝑥 ∈ Fin ) )
11	1 3 10	3bitr4i	⊢ ( 𝑥 ∈ FinVII ↔ 𝑥 ∈ ( Fin ∪ ( V ∖ dom card ) ) )
12	11	eqriv	⊢ FinVII = ( Fin ∪ ( V ∖ dom card ) )