vfinncsp - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > vfinncsp		GIF version

Theorem vfinncsp 4555

Description: If the universe is finite, then the size of Sp_fin is equal to the successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)

**Assertion**
Ref	Expression
vfinncsp	⊢ (V ∈ Fin → Nc_fin Sp_fin = ( T_fin Nc_fin Sp_fin +_c 1_c))

Proof of Theorem vfinncsp Dummy variables x a t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vfinspeqtncv 4554	. . 3 ⊢ (V ∈ Fin → Sp_fin = ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
2		ncfineq 4474	. . 3 ⊢ ( Sp_fin = ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) → Nc_fin Sp_fin = Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
3	1, 2	syl 15	. 2 ⊢ (V ∈ Fin → Nc_fin Sp_fin = Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
4		vfinncvntsp 4550	. . . 4 ⊢ (V ∈ Fin → ¬ Nc_fin V ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x})
5		disjsn 3787	. . . 4 ⊢ (({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∩ { Nc_fin V}) = ∅ ↔ ¬ Nc_fin V ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x})
6	4, 5	sylibr 203	. . 3 ⊢ (V ∈ Fin → ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∩ { Nc_fin V}) = ∅)
7		vex 2863	. . . . . . . . 9 ⊢ a ∈ V
8	7	elimak 4260	. . . . . . . 8 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
9		df-rex 2621	. . . . . . . . 9 ⊢ (∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
10		elpw1 4145	. . . . . . . . . . . . 13 ⊢ (t ∈ ℘₁ Sp_fin ↔ ∃x ∈ Sp_fin t = {x})
11	10	anbi1i 676	. . . . . . . . . . . 12 ⊢ ((t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ (∃x ∈ Sp_fin t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
12		r19.41v 2765	. . . . . . . . . . . 12 ⊢ (∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ (∃x ∈ Sp_fin t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
13	11, 12	bitr4i 243	. . . . . . . . . . 11 ⊢ ((t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
14	13	exbii 1582	. . . . . . . . . 10 ⊢ (∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃t∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
15		rexcom4 2879	. . . . . . . . . 10 ⊢ (∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃t∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
16	14, 15	bitr4i 243	. . . . . . . . 9 ⊢ (∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
17	9, 16	bitri 240	. . . . . . . 8 ⊢ (∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
18	8, 17	bitri 240	. . . . . . 7 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
19		snex 4112	. . . . . . . . . 10 ⊢ {x} ∈ V
20		opkeq1 4060	. . . . . . . . . . 11 ⊢ (t = {x} → ⟪t, a⟫ = ⟪{x}, a⟫)
21	20	eleq1d 2419	. . . . . . . . . 10 ⊢ (t = {x} → (⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
22	19, 21	ceqsexv 2895	. . . . . . . . 9 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
23		vex 2863	. . . . . . . . . 10 ⊢ x ∈ V
24	23, 7	eqtfinrelk 4487	. . . . . . . . 9 ⊢ (⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ a = T_fin x)
25	22, 24	bitri 240	. . . . . . . 8 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ a = T_fin x)
26	25	rexbii 2640	. . . . . . 7 ⊢ (∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin a = T_fin x)
27	18, 26	bitri 240	. . . . . 6 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃x ∈ Sp_fin a = T_fin x)
28	27	abbi2i 2465	. . . . 5 ⊢ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) = {a ∣ ∃x ∈ Sp_fin a = T_fin x}
29		tfinrelkex 4488	. . . . . 6 ⊢ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ∈ V
30		spfinex 4538	. . . . . . 7 ⊢ Sp_fin ∈ V
31	30	pw1ex 4304	. . . . . 6 ⊢ ℘₁ Sp_fin ∈ V
32	29, 31	imakex 4301	. . . . 5 ⊢ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ∈ V
33	28, 32	eqeltrri 2424	. . . 4 ⊢ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ V
34		snex 4112	. . . . 5 ⊢ { Nc_fin V} ∈ V
35		ncfindi 4476	. . . . 5 ⊢ (((V ∈ Fin ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ V) ∧ { Nc_fin V} ∈ V ∧ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∩ { Nc_fin V}) = ∅) → Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) = ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} +_c Nc_fin { Nc_fin V}))
36	34, 35	mp3an2 1265	. . . 4 ⊢ (((V ∈ Fin ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ V) ∧ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∩ { Nc_fin V}) = ∅) → Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) = ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} +_c Nc_fin { Nc_fin V}))
37	33, 36	mpanl2 662	. . 3 ⊢ ((V ∈ Fin ∧ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∩ { Nc_fin V}) = ∅) → Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) = ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} +_c Nc_fin { Nc_fin V}))
38	6, 37	mpdan 649	. 2 ⊢ (V ∈ Fin → Nc_fin ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) = ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} +_c Nc_fin { Nc_fin V}))
39		ncfinprop 4475	. . . . . 6 ⊢ ((V ∈ Fin ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ V) → ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nn ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x}))
40	33, 39	mpan2 652	. . . . 5 ⊢ (V ∈ Fin → ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nn ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x}))
41	40	simpld 445	. . . 4 ⊢ (V ∈ Fin → Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nn )
42		ncfinprop 4475	. . . . . . 7 ⊢ ((V ∈ Fin ∧ Sp_fin ∈ V) → ( Nc_fin Sp_fin ∈ Nn ∧ Sp_fin ∈ Nc_fin Sp_fin ))
43	30, 42	mpan2 652	. . . . . 6 ⊢ (V ∈ Fin → ( Nc_fin Sp_fin ∈ Nn ∧ Sp_fin ∈ Nc_fin Sp_fin ))
44	43	simpld 445	. . . . 5 ⊢ (V ∈ Fin → Nc_fin Sp_fin ∈ Nn )
45		tfincl 4493	. . . . 5 ⊢ ( Nc_fin Sp_fin ∈ Nn → T_fin Nc_fin Sp_fin ∈ Nn )
46	44, 45	syl 15	. . . 4 ⊢ (V ∈ Fin → T_fin Nc_fin Sp_fin ∈ Nn )
47	40	simprd 449	. . . 4 ⊢ (V ∈ Fin → {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x})
48		vfinspnn 4542	. . . . . 6 ⊢ (V ∈ Fin → Sp_fin ⊆ ( Nn ∖ {∅}))
49		difss 3394	. . . . . 6 ⊢ ( Nn ∖ {∅}) ⊆ Nn
50	48, 49	syl6ss 3285	. . . . 5 ⊢ (V ∈ Fin → Sp_fin ⊆ Nn )
51	43	simprd 449	. . . . 5 ⊢ (V ∈ Fin → Sp_fin ∈ Nc_fin Sp_fin )
52		tfinnn 4535	. . . . 5 ⊢ (( Nc_fin Sp_fin ∈ Nn ∧ Sp_fin ⊆ Nn ∧ Sp_fin ∈ Nc_fin Sp_fin ) → {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ T_fin Nc_fin Sp_fin )
53	44, 50, 51, 52	syl3anc 1182	. . . 4 ⊢ (V ∈ Fin → {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ T_fin Nc_fin Sp_fin )
54		nnceleq 4431	. . . 4 ⊢ ((( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nn ∧ T_fin Nc_fin Sp_fin ∈ Nn ) ∧ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∧ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ T_fin Nc_fin Sp_fin )) → Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} = T_fin Nc_fin Sp_fin )
55	41, 46, 47, 53, 54	syl22anc 1183	. . 3 ⊢ (V ∈ Fin → Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} = T_fin Nc_fin Sp_fin )
56		ncfinex 4473	. . . 4 ⊢ Nc_fin V ∈ V
57		ncfinsn 4477	. . . 4 ⊢ ((V ∈ Fin ∧ Nc_fin V ∈ V) → Nc_fin { Nc_fin V} = 1_c)
58	56, 57	mpan2 652	. . 3 ⊢ (V ∈ Fin → Nc_fin { Nc_fin V} = 1_c)
59	55, 58	addceq12d 4392	. 2 ⊢ (V ∈ Fin → ( Nc_fin {a ∣ ∃x ∈ Sp_fin a = T_fin x} +_c Nc_fin { Nc_fin V}) = ( T_fin Nc_fin Sp_fin +_c 1_c))
60	3, 38, 59	3eqtrd 2389	1 ⊢ (V ∈ Fin → Nc_fin Sp_fin = ( T_fin Nc_fin Sp_fin +_c 1_c))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ⊆ wss 3258 ∅c0 3551 ℘cpw 3723 {csn 3738 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 ^◡_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 S_k cssetk 4184 I_k cidk 4185 Nn cnnc 4374 +_c cplc 4376 Fin cfin 4377 Nc_fin cncfin 4435 T_fin ctfin 4436 Sp_fin cspfin 4440

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-13 1712 ax-14 1714 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-sfin 4447 df-spfin 4448

This theorem is referenced by: vinf 4556

W3C validator