evenfinex - New Foundations Explorer

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

Theorem evenfinex 4504

Description: The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)

**Assertion**
Ref	Expression
evenfinex	⊢ Even_fin ∈ V

Proof of Theorem evenfinex Dummy variables a b c n t x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-evenfin 4445	. . 3 ⊢ Even_fin = {x ∣ (∃n ∈ Nn x = (n +_c n) ∧ x ≠ ∅)}
2		eldifsn 3840	. . . . 5 ⊢ (x ∈ (( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∖ {∅}) ↔ (x ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∧ x ≠ ∅))
3		vex 2863	. . . . . . . 8 ⊢ x ∈ V
4	3	elimak 4260	. . . . . . 7 ⊢ (x ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ↔ ∃n ∈ Nn ⟪n, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
5		opkex 4114	. . . . . . . . . . . 12 ⊢ ⟪n, x⟫ ∈ V
6	5	elimak 4260	. . . . . . . . . . 11 ⊢ (⟪n, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)))
7		elpw121c 4149	. . . . . . . . . . . . . . 15 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃a t = {{{a}}})
8	7	anbi1i 676	. . . . . . . . . . . . . 14 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ (∃a t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
9		19.41v 1901	. . . . . . . . . . . . . 14 ⊢ (∃a(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ (∃a t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
10	8, 9	bitr4i 243	. . . . . . . . . . . . 13 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ∃a(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
11	10	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ∃t∃a(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
12		df-rex 2621	. . . . . . . . . . . 12 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
13		excom 1741	. . . . . . . . . . . 12 ⊢ (∃a∃t(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ∃t∃a(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
14	11, 12, 13	3bitr4i 268	. . . . . . . . . . 11 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ ∃a∃t(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
15		snex 4112	. . . . . . . . . . . . . 14 ⊢ {{{a}}} ∈ V
16		opkeq1 4060	. . . . . . . . . . . . . . 15 ⊢ (t = {{{a}}} → ⟪t, ⟪n, x⟫⟫ = ⟪{{{a}}}, ⟪n, x⟫⟫)
17	16	eleq1d 2419	. . . . . . . . . . . . . 14 ⊢ (t = {{{a}}} → (⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))))
18	15, 17	ceqsexv 2895	. . . . . . . . . . . . 13 ⊢ (∃t(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)))
19		elsymdif 3224	. . . . . . . . . . . . 13 ⊢ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ ¬ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)))
20		snex 4112	. . . . . . . . . . . . . . . . 17 ⊢ {a} ∈ V
21		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ n ∈ V
22	20, 21, 3	otkelins2k 4256	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{a}, x⟫ ∈ S_k )
23		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ a ∈ V
24	23, 3	elssetk 4271	. . . . . . . . . . . . . . . 16 ⊢ (⟪{a}, x⟫ ∈ S_k ↔ a ∈ x)
25	22, 24	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins2_k S_k ↔ a ∈ x)
26		opkex 4114	. . . . . . . . . . . . . . . . . 18 ⊢ ⟪{a}, n⟫ ∈ V
27	26	elimak 4260	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{a}, n⟫ ∈ (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c))
28		df-rex 2621	. . . . . . . . . . . . . . . . 17 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
29		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃c t = {{{c}}})
30	29	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ (∃c t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
31		19.41v 1901	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃c(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ (∃c t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
32	30, 31	bitr4i 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃c(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
33	32	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃t∃c(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
34		excom 1741	. . . . . . . . . . . . . . . . . 18 ⊢ (∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃t∃c(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
35	33, 34	bitr4i 243	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
36	27, 28, 35	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (⟪{a}, n⟫ ∈ (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ↔ ∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
37	20, 21, 3	otkelins3k 4257	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ↔ ⟪{a}, n⟫ ∈ (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))
38		eladdc 4399	. . . . . . . . . . . . . . . . 17 ⊢ (a ∈ (n +_c n) ↔ ∃b ∈ n ∃c ∈ n ((b ∩ c) = ∅ ∧ a = (b ∪ c)))
39		r2ex 2653	. . . . . . . . . . . . . . . . 17 ⊢ (∃b ∈ n ∃c ∈ n ((b ∩ c) = ∅ ∧ a = (b ∪ c)) ↔ ∃b∃c((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
40		excom 1741	. . . . . . . . . . . . . . . . . 18 ⊢ (∃b∃c((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))) ↔ ∃c∃b((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
41		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {{{c}}} ∈ V
42		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = {{{c}}} → ⟪t, ⟪{a}, n⟫⟫ = ⟪{{{c}}}, ⟪{a}, n⟫⟫)
43	42	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = {{{c}}} → (⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
44	41, 43	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c))
45		opkex 4114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ V
46	45	elimak 4260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))))
47		df-rex 2621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) ↔ ∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
48		elpw141c 4151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t ∈ ℘₁℘₁℘₁℘₁1_c ↔ ∃b t = {{{{{b}}}}})
49	48	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ (∃b t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
50		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃b(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ (∃b t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
51	49, 50	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ∃b(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ∃t∃b(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
53		excom 1741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃b∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ∃t∃b(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
54	52, 53	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ∃b∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
55	46, 47, 54	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃b∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
56		snex 4112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {{{{{b}}}}} ∈ V
57		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = {{{{{b}}}}} → ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ = ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫)
58	57	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t = {{{{{b}}}}} → (⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) ↔ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))))
59	56, 58	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))))
60		elin 3220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))))
61		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (V ×_k Ins2_k S_k )))
62		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {{{b}}} ∈ V
63	62, 41, 26	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{b}}}, ⟪{a}, n⟫⟫ ∈ Ins2_k S_k )
64		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {b} ∈ V
65	64, 20, 21	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{b}}}, ⟪{a}, n⟫⟫ ∈ Ins2_k S_k ↔ ⟪{b}, n⟫ ∈ S_k )
66		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ b ∈ V
67	66, 21	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{b}, n⟫ ∈ S_k ↔ b ∈ n)
68	63, 65, 67	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ b ∈ n)
69	56, 45	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (V ×_k Ins2_k S_k ) ↔ ({{{{{b}}}}} ∈ V ∧ ⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ Ins2_k S_k ))
70	56, 69	mpbiran 884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (V ×_k Ins2_k S_k ) ↔ ⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ Ins2_k S_k )
71		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {c} ∈ V
72	71, 20, 21	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{c}}}, ⟪{a}, n⟫⟫ ∈ Ins2_k S_k ↔ ⟪{c}, n⟫ ∈ S_k )
73		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ c ∈ V
74	73, 21	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{c}, n⟫ ∈ S_k ↔ c ∈ n)
75	70, 72, 74	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (V ×_k Ins2_k S_k ) ↔ c ∈ n)
76	68, 75	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (V ×_k Ins2_k S_k )) ↔ (b ∈ n ∧ c ∈ n))
77	61, 76	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ↔ (b ∈ n ∧ c ∈ n))
78		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))
79	62, 41, 26	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{{{b}}}, {{{c}}}⟫ ∈ SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
80		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {{b}} ∈ V
81		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {{c}} ∈ V
82	80, 81	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{b}}}, {{{c}}}⟫ ∈ SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{{b}}, {{c}}⟫ ∈ SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
83	64, 71	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{b}}, {{c}}⟫ ∈ SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{b}, {c}⟫ ∈ SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
84	66, 73	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{b}, {c}⟫ ∈ SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪b, c⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
85	66, 73	ndisjrelk 4324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪b, c⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (b ∩ c) ≠ ∅)
86	85	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ ⟪b, c⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ (b ∩ c) ≠ ∅)
87		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟪b, c⟫ ∈ V
88	87	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪b, c⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ ⟪b, c⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
89		df-ne 2519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((b ∩ c) ≠ ∅ ↔ ¬ (b ∩ c) = ∅)
90	89	con2bii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((b ∩ c) = ∅ ↔ ¬ (b ∩ c) ≠ ∅)
91	86, 88, 90	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪b, c⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (b ∩ c) = ∅)
92	83, 84, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{b}}, {{c}}⟫ ∈ SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (b ∩ c) = ∅)
93	79, 82, 92	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (b ∩ c) = ∅)
94		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ V
95	94	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )))
96		elpw171c 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ↔ ∃x t = {{{{{{{{x}}}}}}}})
97	96	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
98		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃x(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
99	97, 98	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ∃x(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
100	99	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ∃t∃x(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
101		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ ∃t(t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
102		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃x∃t(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ∃t∃x(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
103	100, 101, 102	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ ∃x∃t(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
104		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {{{{{{{{x}}}}}}}} ∈ V
105		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (t = {{{{{{{{x}}}}}}}} → ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ = ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫)
106	105	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t = {{{{{{{{x}}}}}}}} → (⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))))
107	104, 106	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃t(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )))
108		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ ¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )))
109		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {{{{{{x}}}}}} ∈ V
110	109, 56, 45	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k )
111		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {{{{x}}}} ∈ V
112	111, 41, 26	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ∈ Ins3_k SI_k S_k )
113		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {{x}} ∈ V
114	113, 20, 21	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ∈ Ins3_k SI_k S_k ↔ ⟪{{x}}, {a}⟫ ∈ SI_k S_k )
115		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {x} ∈ V
116	115, 23	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{x}}, {a}⟫ ∈ SI_k S_k ↔ ⟪{x}, a⟫ ∈ S_k )
117	3, 23	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{x}, a⟫ ∈ S_k ↔ x ∈ a)
118	114, 116, 117	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ∈ Ins3_k SI_k S_k ↔ x ∈ a)
119	110, 112, 118	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins2_k Ins3_k SI_k S_k ↔ x ∈ a)
120	109, 56, 45	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{x}}}}}}, {{{{{b}}}}}⟫ ∈ SI_k SI_k SI_k SI_k SI_k S_k )
121		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {{{{{x}}}}} ∈ V
122		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {{{{b}}}} ∈ V
123	121, 122	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{x}}}}}}, {{{{{b}}}}}⟫ ∈ SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{x}}}}}, {{{{b}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k )
124	111, 62	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{{x}}}}}, {{{{b}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{x}}}}, {{{b}}}⟫ ∈ SI_k SI_k SI_k S_k )
125		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ {{{x}}} ∈ V
126	125, 80	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{x}}}}, {{{b}}}⟫ ∈ SI_k SI_k SI_k S_k ↔ ⟪{{{x}}}, {{b}}⟫ ∈ SI_k SI_k S_k )
127	113, 64	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{x}}}, {{b}}⟫ ∈ SI_k SI_k S_k ↔ ⟪{{x}}, {b}⟫ ∈ SI_k S_k )
128	115, 66	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{x}}, {b}⟫ ∈ SI_k S_k ↔ ⟪{x}, b⟫ ∈ S_k )
129	3, 66	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{x}, b⟫ ∈ S_k ↔ x ∈ b)
130	127, 128, 129	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{x}}}, {{b}}⟫ ∈ SI_k SI_k S_k ↔ x ∈ b)
131	124, 126, 130	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{x}}}}}, {{{{b}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k ↔ x ∈ b)
132	120, 123, 131	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ x ∈ b)
133	109, 56, 45	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k S_k )
134	111, 41, 26	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k S_k ↔ ⟪{{{{x}}}}, {{{c}}}⟫ ∈ SI_k SI_k SI_k S_k )
135	125, 81	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{x}}}}, {{{c}}}⟫ ∈ SI_k SI_k SI_k S_k ↔ ⟪{{{x}}}, {{c}}⟫ ∈ SI_k SI_k S_k )
136	113, 71	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{x}}}, {{c}}⟫ ∈ SI_k SI_k S_k ↔ ⟪{{x}}, {c}⟫ ∈ SI_k S_k )
137	115, 73	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{x}}, {c}⟫ ∈ SI_k S_k ↔ ⟪{x}, c⟫ ∈ S_k )
138	3, 73	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{x}, c⟫ ∈ S_k ↔ x ∈ c)
139	137, 138	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{x}}, {c}⟫ ∈ SI_k S_k ↔ x ∈ c)
140	135, 136, 139	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{x}}}}, {{{c}}}⟫ ∈ SI_k SI_k SI_k S_k ↔ x ∈ c)
141	133, 134, 140	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k SI_k SI_k S_k ↔ x ∈ c)
142	132, 141	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∨ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k SI_k SI_k S_k ) ↔ (x ∈ b ∨ x ∈ c))
143		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ) ↔ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∨ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))
144		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (x ∈ (b ∪ c) ↔ (x ∈ b ∨ x ∈ c))
145	142, 143, 144	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ) ↔ x ∈ (b ∪ c))
146	119, 145	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ (x ∈ a ↔ x ∈ (b ∪ c)))
147	146	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ Ins2_k Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ↔ ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
148	107, 108, 147	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
149	148	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃x∃t(t = {{{{{{{{x}}}}}}}} ∧ ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ∈ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ))) ↔ ∃x ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
150	95, 103, 149	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ∃x ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
151	150	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ¬ ∃x ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
152	94	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ¬ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))
153		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (a = (b ∪ c) ↔ ∀x(x ∈ a ↔ x ∈ (b ∪ c)))
154		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀x(x ∈ a ↔ x ∈ (b ∪ c)) ↔ ¬ ∃x ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
155	153, 154	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (a = (b ∪ c) ↔ ¬ ∃x ¬ (x ∈ a ↔ x ∈ (b ∪ c)))
156	151, 152, 155	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ a = (b ∪ c))
157	93, 156	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)) ↔ ((b ∩ c) = ∅ ∧ a = (b ∪ c)))
158	78, 157	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)) ↔ ((b ∩ c) = ∅ ∧ a = (b ∪ c)))
159	77, 158	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∧ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) ↔ ((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
160	59, 60, 159	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
161	160	exbii 1582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃b∃t(t = {{{{{b}}}}} ∧ ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∈ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)))) ↔ ∃b((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
162	44, 55, 161	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃b((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
163	162	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃c∃b((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))))
164	40, 163	bitr4i 243	. . . . . . . . . . . . . . . . 17 ⊢ (∃b∃c((b ∈ n ∧ c ∈ n) ∧ ((b ∩ c) = ∅ ∧ a = (b ∪ c))) ↔ ∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
165	38, 39, 164	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (a ∈ (n +_c n) ↔ ∃c∃t(t = {{{c}}} ∧ ⟪t, ⟪{a}, n⟫⟫ ∈ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)))
166	36, 37, 165	3bitr4i 268	. . . . . . . . . . . . . . 15 ⊢ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ↔ a ∈ (n +_c n))
167	25, 166	bibi12i 306	. . . . . . . . . . . . . 14 ⊢ ((⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ (a ∈ x ↔ a ∈ (n +_c n)))
168	167	notbii 287	. . . . . . . . . . . . 13 ⊢ (¬ (⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ∈ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ↔ ¬ (a ∈ x ↔ a ∈ (n +_c n)))
169	18, 19, 168	3bitri 262	. . . . . . . . . . . 12 ⊢ (∃t(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ¬ (a ∈ x ↔ a ∈ (n +_c n)))
170	169	exbii 1582	. . . . . . . . . . 11 ⊢ (∃a∃t(t = {{{a}}} ∧ ⟪t, ⟪n, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c))) ↔ ∃a ¬ (a ∈ x ↔ a ∈ (n +_c n)))
171	6, 14, 170	3bitri 262	. . . . . . . . . 10 ⊢ (⟪n, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃a ¬ (a ∈ x ↔ a ∈ (n +_c n)))
172	171	notbii 287	. . . . . . . . 9 ⊢ (¬ ⟪n, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ∃a ¬ (a ∈ x ↔ a ∈ (n +_c n)))
173	5	elcompl 3226	. . . . . . . . 9 ⊢ (⟪n, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ⟪n, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
174		dfcleq 2347	. . . . . . . . . 10 ⊢ (x = (n +_c n) ↔ ∀a(a ∈ x ↔ a ∈ (n +_c n)))
175		alex 1572	. . . . . . . . . 10 ⊢ (∀a(a ∈ x ↔ a ∈ (n +_c n)) ↔ ¬ ∃a ¬ (a ∈ x ↔ a ∈ (n +_c n)))
176	174, 175	bitri 240	. . . . . . . . 9 ⊢ (x = (n +_c n) ↔ ¬ ∃a ¬ (a ∈ x ↔ a ∈ (n +_c n)))
177	172, 173, 176	3bitr4i 268	. . . . . . . 8 ⊢ (⟪n, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ x = (n +_c n))
178	177	rexbii 2640	. . . . . . 7 ⊢ (∃n ∈ Nn ⟪n, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃n ∈ Nn x = (n +_c n))
179	4, 178	bitri 240	. . . . . 6 ⊢ (x ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ↔ ∃n ∈ Nn x = (n +_c n))
180	179	anbi1i 676	. . . . 5 ⊢ ((x ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∧ x ≠ ∅) ↔ (∃n ∈ Nn x = (n +_c n) ∧ x ≠ ∅))
181	2, 180	bitri 240	. . . 4 ⊢ (x ∈ (( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∖ {∅}) ↔ (∃n ∈ Nn x = (n +_c n) ∧ x ≠ ∅))
182	181	abbi2i 2465	. . 3 ⊢ (( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∖ {∅}) = {x ∣ (∃n ∈ Nn x = (n +_c n) ∧ x ≠ ∅)}
183	1, 182	eqtr4i 2376	. 2 ⊢ Even_fin = (( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∖ {∅})
184		ssetkex 4295	. . . . . . . 8 ⊢ S_k ∈ V
185	184	ins2kex 4308	. . . . . . 7 ⊢ Ins2_k S_k ∈ V
186	185	ins2kex 4308	. . . . . . . . . . . 12 ⊢ Ins2_k Ins2_k S_k ∈ V
187		vvex 4110	. . . . . . . . . . . . 13 ⊢ V ∈ V
188	187, 185	xpkex 4290	. . . . . . . . . . . 12 ⊢ (V ×_k Ins2_k S_k ) ∈ V
189	186, 188	inex 4106	. . . . . . . . . . 11 ⊢ ( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∈ V
190	184	ins3kex 4309	. . . . . . . . . . . . . . . . . . 19 ⊢ Ins3_k S_k ∈ V
191	190, 185	inex 4106	. . . . . . . . . . . . . . . . . 18 ⊢ ( Ins3_k S_k ∩ Ins2_k S_k ) ∈ V
192		1cex 4143	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1_c ∈ V
193	192	pw1ex 4304	. . . . . . . . . . . . . . . . . . 19 ⊢ ℘₁1_c ∈ V
194	193	pw1ex 4304	. . . . . . . . . . . . . . . . . 18 ⊢ ℘₁℘₁1_c ∈ V
195	191, 194	imakex 4301	. . . . . . . . . . . . . . . . 17 ⊢ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
196	195	complex 4105	. . . . . . . . . . . . . . . 16 ⊢ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
197	196	sikex 4298	. . . . . . . . . . . . . . 15 ⊢ SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
198	197	sikex 4298	. . . . . . . . . . . . . 14 ⊢ SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
199	198	sikex 4298	. . . . . . . . . . . . 13 ⊢ SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
200	199	ins3kex 4309	. . . . . . . . . . . 12 ⊢ Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
201	184	sikex 4298	. . . . . . . . . . . . . . . . . 18 ⊢ SI_k S_k ∈ V
202	201	ins3kex 4309	. . . . . . . . . . . . . . . . 17 ⊢ Ins3_k SI_k S_k ∈ V
203	202	ins2kex 4308	. . . . . . . . . . . . . . . 16 ⊢ Ins2_k Ins3_k SI_k S_k ∈ V
204	203	ins2kex 4308	. . . . . . . . . . . . . . 15 ⊢ Ins2_k Ins2_k Ins3_k SI_k S_k ∈ V
205	201	sikex 4298	. . . . . . . . . . . . . . . . . . . 20 ⊢ SI_k SI_k S_k ∈ V
206	205	sikex 4298	. . . . . . . . . . . . . . . . . . 19 ⊢ SI_k SI_k SI_k S_k ∈ V
207	206	sikex 4298	. . . . . . . . . . . . . . . . . 18 ⊢ SI_k SI_k SI_k SI_k S_k ∈ V
208	207	sikex 4298	. . . . . . . . . . . . . . . . 17 ⊢ SI_k SI_k SI_k SI_k SI_k S_k ∈ V
209	208	ins3kex 4309	. . . . . . . . . . . . . . . 16 ⊢ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∈ V
210	206	ins3kex 4309	. . . . . . . . . . . . . . . . 17 ⊢ Ins3_k SI_k SI_k SI_k S_k ∈ V
211	210	ins2kex 4308	. . . . . . . . . . . . . . . 16 ⊢ Ins2_k Ins3_k SI_k SI_k SI_k S_k ∈ V
212	209, 211	unex 4107	. . . . . . . . . . . . . . 15 ⊢ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k ) ∈ V
213	204, 212	symdifex 4109	. . . . . . . . . . . . . 14 ⊢ ( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) ∈ V
214	194	pw1ex 4304	. . . . . . . . . . . . . . . . . 18 ⊢ ℘₁℘₁℘₁1_c ∈ V
215	214	pw1ex 4304	. . . . . . . . . . . . . . . . 17 ⊢ ℘₁℘₁℘₁℘₁1_c ∈ V
216	215	pw1ex 4304	. . . . . . . . . . . . . . . 16 ⊢ ℘₁℘₁℘₁℘₁℘₁1_c ∈ V
217	216	pw1ex 4304	. . . . . . . . . . . . . . 15 ⊢ ℘₁℘₁℘₁℘₁℘₁℘₁1_c ∈ V
218	217	pw1ex 4304	. . . . . . . . . . . . . 14 ⊢ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∈ V
219	213, 218	imakex 4301	. . . . . . . . . . . . 13 ⊢ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∈ V
220	219	complex 4105	. . . . . . . . . . . 12 ⊢ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∈ V
221	200, 220	inex 4106	. . . . . . . . . . 11 ⊢ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c)) ∈ V
222	189, 221	inex 4106	. . . . . . . . . 10 ⊢ (( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) ∈ V
223	222, 215	imakex 4301	. . . . . . . . 9 ⊢ ((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ∈ V
224	223, 194	imakex 4301	. . . . . . . 8 ⊢ (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ∈ V
225	224	ins3kex 4309	. . . . . . 7 ⊢ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c) ∈ V
226	185, 225	symdifex 4109	. . . . . 6 ⊢ ( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) ∈ V
227	226, 194	imakex 4301	. . . . 5 ⊢ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
228	227	complex 4105	. . . 4 ⊢ ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
229		nncex 4397	. . . 4 ⊢ Nn ∈ V
230	228, 229	imakex 4301	. . 3 ⊢ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∈ V
231		snex 4112	. . 3 ⊢ {∅} ∈ V
232	230, 231	difex 4108	. 2 ⊢ (( ∼ (( Ins2_k S_k ⊕ Ins3_k (((( Ins2_k Ins2_k S_k ∩ (V ×_k Ins2_k S_k )) ∩ ( Ins3_k SI_k SI_k SI_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ ∼ (( Ins2_k Ins2_k Ins3_k SI_k S_k ⊕ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∪ Ins2_k Ins3_k SI_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k Nn ) ∖ {∅}) ∈ V
233	183, 232	eqeltri 2423	1 ⊢ Even_fin ∈ V

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ≠ wne 2517 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ∅c0 3551 {csn 3738 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 S_k cssetk 4184 Nn cnnc 4374 +_c cplc 4376 Even_fin cevenfin 4437

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-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-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 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-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-addc 4379 df-nnc 4380 df-evenfin 4445

This theorem is referenced by: evenoddnnnul 4515

W3C validator