nnsucelrlem1 - New Foundations Explorer

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

Theorem nnsucelrlem1 4425

Description: Lemma for nnsucelr 4429. Establish stratification for the inductive hypothesis. (Contributed by SF, 15-Jan-2015.)

**Assertion**
Ref	Expression
nnsucelrlem1	⊢ {m ∣ ∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m)} ∈ V

Distinct variable group: m,a,x

Proof of Theorem nnsucelrlem1 Dummy variables e t w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . . . . 8 ⊢ m ∈ V
2	1	elimak 4260	. . . . . . 7 ⊢ (m ∈ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ∃t ∈ 1_c ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c))
3		df-rex 2621	. . . . . . . 8 ⊢ (∃t ∈ 1_c ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ∃t(t ∈ 1_c ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
4		el1c 4140	. . . . . . . . . . . 12 ⊢ (t ∈ 1_c ↔ ∃a t = {a})
5	4	anbi1i 676	. . . . . . . . . . 11 ⊢ ((t ∈ 1_c ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ (∃a t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
6		19.41v 1901	. . . . . . . . . . 11 ⊢ (∃a(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ (∃a t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
7	5, 6	bitr4i 243	. . . . . . . . . 10 ⊢ ((t ∈ 1_c ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ∃a(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
8	7	exbii 1582	. . . . . . . . 9 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ∃t∃a(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
9		excom 1741	. . . . . . . . 9 ⊢ (∃a∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ∃t∃a(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
10	8, 9	bitr4i 243	. . . . . . . 8 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ∃a∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
11	3, 10	bitri 240	. . . . . . 7 ⊢ (∃t ∈ 1_c ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ∃a∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
12	2, 11	bitri 240	. . . . . 6 ⊢ (m ∈ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ∃a∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
13		snex 4112	. . . . . . . . 9 ⊢ {a} ∈ V
14		opkeq1 4060	. . . . . . . . . 10 ⊢ (t = {a} → ⟪t, m⟫ = ⟪{a}, m⟫)
15	14	eleq1d 2419	. . . . . . . . 9 ⊢ (t = {a} → (⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)))
16	13, 15	ceqsexv 2895	. . . . . . . 8 ⊢ (∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c))
17		opkex 4114	. . . . . . . . . . . 12 ⊢ ⟪{a}, m⟫ ∈ V
18	17	elimak 4260	. . . . . . . . . . 11 ⊢ (⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )))
19		df-rex 2621	. . . . . . . . . . . 12 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ ∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
20		elpw131c 4150	. . . . . . . . . . . . . . . 16 ⊢ (t ∈ ℘₁℘₁℘₁1_c ↔ ∃x t = {{{{x}}}})
21	20	anbi1i 676	. . . . . . . . . . . . . . 15 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ (∃x t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
22		19.41v 1901	. . . . . . . . . . . . . . 15 ⊢ (∃x(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ (∃x t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
23	21, 22	bitr4i 243	. . . . . . . . . . . . . 14 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ∃x(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
24	23	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ∃t∃x(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
25		excom 1741	. . . . . . . . . . . . 13 ⊢ (∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ∃t∃x(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
26	24, 25	bitr4i 243	. . . . . . . . . . . 12 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
27	19, 26	bitri 240	. . . . . . . . . . 11 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ ∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
28	18, 27	bitri 240	. . . . . . . . . 10 ⊢ (⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
29		snex 4112	. . . . . . . . . . . . 13 ⊢ {{{{x}}}} ∈ V
30		opkeq1 4060	. . . . . . . . . . . . . 14 ⊢ (t = {{{{x}}}} → ⟪t, ⟪{a}, m⟫⟫ = ⟪{{{{x}}}}, ⟪{a}, m⟫⟫)
31	30	eleq1d 2419	. . . . . . . . . . . . 13 ⊢ (t = {{{{x}}}} → (⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))))
32	29, 31	ceqsexv 2895	. . . . . . . . . . . 12 ⊢ (∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )))
33		eldif 3222	. . . . . . . . . . . . . 14 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k )))
34		eldif 3222	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ))
35		opkex 4114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ V
36	35	elimak 4260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )))
37		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ ∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
38		elpw141c 4151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t ∈ ℘₁℘₁℘₁℘₁1_c ↔ ∃w t = {{{{{w}}}}})
39	38	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ (∃w t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
40		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ (∃w t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
41	39, 40	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
42	41	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ∃t∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
43		excom 1741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ∃t∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
44	42, 43	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
45	37, 44	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ ∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
46		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {{{{{w}}}}} ∈ V
47		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t = {{{{{w}}}}} → ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ = ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫)
48	47	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = {{{{{w}}}}} → (⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))))
49	46, 48	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )))
50		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∧ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )))
51		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ V
52	51	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )))
53		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ∃t(t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
54		elpw171c 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ↔ ∃e t = {{{{{{{{e}}}}}}}})
55	54	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ (∃e t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
56		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃e(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ (∃e t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
57	55, 56	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ∃e(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
58	57	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ∃t∃e(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
59		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃e∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ∃t∃e(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
60	58, 59	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ∃e∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
61	53, 60	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁℘₁℘₁℘₁1_c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ∃e∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
62	52, 61	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ∃e∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
63		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {{{{{{{{e}}}}}}}} ∈ V
64		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (t = {{{{{{{{e}}}}}}}} → ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ = ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫)
65	64	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t = {{{{{{{{e}}}}}}}} → (⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))))
66	63, 65	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )))
67		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ¬ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )))
68		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {{{{{{e}}}}}} ∈ V
69	68, 46, 35	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ ∈ SI_k SI_k SI_k SI_k SI_k S_k )
70		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {{{{{e}}}}} ∈ V
71		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {{{{w}}}} ∈ V
72	70, 71	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ ∈ SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k )
73		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ {{{{e}}}} ∈ V
74		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ {{{w}}} ∈ V
75	73, 74	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{e}}}}, {{{w}}}⟫ ∈ SI_k SI_k SI_k S_k )
76		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {{{e}}} ∈ V
77		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {{w}} ∈ V
78	76, 77	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{{e}}}}, {{{w}}}⟫ ∈ SI_k SI_k SI_k S_k ↔ ⟪{{{e}}}, {{w}}⟫ ∈ SI_k SI_k S_k )
79		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ {{e}} ∈ V
80		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ {w} ∈ V
81	79, 80	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{{e}}}, {{w}}⟫ ∈ SI_k SI_k S_k ↔ ⟪{{e}}, {w}⟫ ∈ SI_k S_k )
82		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ {e} ∈ V
83		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ w ∈ V
84	82, 83	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{{e}}, {w}⟫ ∈ SI_k S_k ↔ ⟪{e}, w⟫ ∈ S_k )
85		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ e ∈ V
86	85, 83	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{e}, w⟫ ∈ S_k ↔ e ∈ w)
87	84, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{e}}, {w}⟫ ∈ SI_k S_k ↔ e ∈ w)
88	81, 87	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{e}}}, {{w}}⟫ ∈ SI_k SI_k S_k ↔ e ∈ w)
89	78, 88	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{e}}}}, {{{w}}}⟫ ∈ SI_k SI_k SI_k S_k ↔ e ∈ w)
90	75, 89	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈ SI_k SI_k SI_k SI_k S_k ↔ e ∈ w)
91	72, 90	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ ∈ SI_k SI_k SI_k SI_k SI_k S_k ↔ e ∈ w)
92	69, 91	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ e ∈ w)
93	68, 46, 35	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ↔ ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))
94	73, 29, 17	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k ↔ ⟪{{{{e}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k )
95	79, 13, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{{{e}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ↔ ⟪{{e}}, {a}⟫ ∈ SI_k S_k )
96		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ a ∈ V
97	82, 96	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{{e}}, {a}⟫ ∈ SI_k S_k ↔ ⟪{e}, a⟫ ∈ S_k )
98	85, 96	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{e}, a⟫ ∈ S_k ↔ e ∈ a)
99	97, 98	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{e}}, {a}⟫ ∈ SI_k S_k ↔ e ∈ a)
100	95, 99	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{{e}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ↔ e ∈ a)
101	94, 100	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k ↔ e ∈ a)
102	73, 29, 17	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3_k I_k ↔ ⟪{{{{e}}}}, {{{{x}}}}⟫ ∈ I_k )
103	76	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ({{{{e}}}} = {{{{x}}}} ↔ {{{e}}} = {{{x}}})
104	79	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ({{{e}}} = {{{x}}} ↔ {{e}} = {{x}})
105	82	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ({{e}} = {{x}} ↔ {e} = {x})
106	85	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ({e} = {x} ↔ e = x)
107	105, 106	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ({{e}} = {{x}} ↔ e = x)
108	104, 107	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ({{{e}}} = {{{x}}} ↔ e = x)
109	103, 108	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ({{{{e}}}} = {{{{x}}}} ↔ e = x)
110		opkelidkg 4275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (({{{{e}}}} ∈ V ∧ {{{{x}}}} ∈ V) → (⟪{{{{e}}}}, {{{{x}}}}⟫ ∈ I_k ↔ {{{{e}}}} = {{{{x}}}}))
111	73, 29, 110	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{{{e}}}}, {{{{x}}}}⟫ ∈ I_k ↔ {{{{e}}}} = {{{{x}}}})
112	85	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (e ∈ {x} ↔ e = x)
113	109, 111, 112	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{{e}}}}, {{{{x}}}}⟫ ∈ I_k ↔ e ∈ {x})
114	102, 113	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3_k I_k ↔ e ∈ {x})
115	101, 114	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k ∨ ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3_k I_k ) ↔ (e ∈ a ∨ e ∈ {x}))
116		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ↔ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins3_k SI_k S_k ∨ ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3_k I_k ))
117		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (e ∈ (a ∪ {x}) ↔ (e ∈ a ∨ e ∈ {x}))
118	115, 116, 117	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ↔ e ∈ (a ∪ {x}))
119	93, 118	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ↔ e ∈ (a ∪ {x}))
120	92, 119	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ (e ∈ w ↔ e ∈ (a ∪ {x})))
121	120	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
122	67, 121	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ↔ ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
123	66, 122	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
124	123	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃e∃t(t = {{{{{{{{e}}}}}}}} ∧ ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ))) ↔ ∃e ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
125	62, 124	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ∃e ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
126	125	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ¬ ∃e ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
127	51	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ ¬ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c))
128		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w = (a ∪ {x}) ↔ ∀e(e ∈ w ↔ e ∈ (a ∪ {x})))
129		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀e(e ∈ w ↔ e ∈ (a ∪ {x})) ↔ ¬ ∃e ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
130	128, 129	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = (a ∪ {x}) ↔ ¬ ∃e ¬ (e ∈ w ↔ e ∈ (a ∪ {x})))
131	126, 127, 130	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ↔ w = (a ∪ {x}))
132	74, 29, 17	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ ⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈ Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))
133	80, 13, 1	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈ Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ ⟪{w}, m⟫ ∈ (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))
134		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⟪{w}, t⟫ ∈ S_k ∧ ⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ (⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ⟪{w}, t⟫ ∈ S_k ))
135		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ t ∈ V
136	135, 1	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ⟪m, t⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
137		opkelimagekg 4272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((m ∈ V ∧ t ∈ V) → (⟪m, t⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ t = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k m)))
138	1, 135, 137	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪m, t⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ t = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k m))
139		dfaddc2 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (m +_c 1_c) = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k m)
140	139	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (t = (m +_c 1_c) ↔ t = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k m))
141	140	bicomi 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (t = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) “_k m) ↔ t = (m +_c 1_c))
142	138, 141	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟪m, t⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ t = (m +_c 1_c))
143	136, 142	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ t = (m +_c 1_c))
144	83, 135	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{w}, t⟫ ∈ S_k ↔ w ∈ t)
145	143, 144	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ⟪{w}, t⟫ ∈ S_k ) ↔ (t = (m +_c 1_c) ∧ w ∈ t))
146	134, 145	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟪{w}, t⟫ ∈ S_k ∧ ⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ (t = (m +_c 1_c) ∧ w ∈ t))
147	146	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(⟪{w}, t⟫ ∈ S_k ∧ ⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ∃t(t = (m +_c 1_c) ∧ w ∈ t))
148	80, 1	opkelcok 4263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{w}, m⟫ ∈ (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ ∃t(⟪{w}, t⟫ ∈ S_k ∧ ⟪t, m⟫ ∈ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c)))
149		1cex 4143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1_c ∈ V
150	1, 149	addcex 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (m +_c 1_c) ∈ V
151	150	clel3 2978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (w ∈ (m +_c 1_c) ↔ ∃t(t = (m +_c 1_c) ∧ w ∈ t))
152	147, 148, 151	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{w}, m⟫ ∈ (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ w ∈ (m +_c 1_c))
153	133, 152	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈ Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ w ∈ (m +_c 1_c))
154	132, 153	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ↔ w ∈ (m +_c 1_c))
155	131, 154	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∧ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ (w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
156	50, 155	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ (w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
157	49, 156	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ (w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
158	157	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ))) ↔ ∃w(w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
159	45, 158	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ↔ ∃w(w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
160	36, 159	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃w(w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
161		df-clel 2349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((a ∪ {x}) ∈ (m +_c 1_c) ↔ ∃w(w = (a ∪ {x}) ∧ w ∈ (m +_c 1_c)))
162	160, 161	bitr4i 243	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ (a ∪ {x}) ∈ (m +_c 1_c))
163		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {{x}} ∈ V
164	163, 13, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ↔ ⟪{{x}}, {a}⟫ ∈ SI_k S_k )
165		snex 4112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {x} ∈ V
166	165, 96	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{x}}, {a}⟫ ∈ SI_k S_k ↔ ⟪{x}, a⟫ ∈ S_k )
167		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ x ∈ V
168	167, 96	elssetk 4271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{x}, a⟫ ∈ S_k ↔ x ∈ a)
169	166, 168	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{x}}, {a}⟫ ∈ SI_k S_k ↔ x ∈ a)
170	164, 169	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ↔ x ∈ a)
171	170	notbii 287	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ↔ ¬ x ∈ a)
172	162, 171	anbi12i 678	. . . . . . . . . . . . . . . . 17 ⊢ ((⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3_k SI_k S_k ) ↔ ((a ∪ {x}) ∈ (m +_c 1_c) ∧ ¬ x ∈ a))
173	34, 172	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ↔ ((a ∪ {x}) ∈ (m +_c 1_c) ∧ ¬ x ∈ a))
174		ancom 437	. . . . . . . . . . . . . . . 16 ⊢ (((a ∪ {x}) ∈ (m +_c 1_c) ∧ ¬ x ∈ a) ↔ (¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)))
175	173, 174	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ↔ (¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)))
176	29, 17	opkelxpk 4249	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k ) ↔ ({{{{x}}}} ∈ V ∧ ⟪{a}, m⟫ ∈ S_k ))
177	29, 176	mpbiran 884	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k ) ↔ ⟪{a}, m⟫ ∈ S_k )
178	96, 1	elssetk 4271	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{a}, m⟫ ∈ S_k ↔ a ∈ m)
179	177, 178	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k ) ↔ a ∈ m)
180	179	notbii 287	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k ) ↔ ¬ a ∈ m)
181	175, 180	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×_k S_k )) ↔ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) ∧ ¬ a ∈ m))
182	33, 181	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) ∧ ¬ a ∈ m))
183		annim 414	. . . . . . . . . . . . 13 ⊢ (((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) ∧ ¬ a ∈ m) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
184	182, 183	bitri 240	. . . . . . . . . . . 12 ⊢ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
185	32, 184	bitri 240	. . . . . . . . . . 11 ⊢ (∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
186	185	exbii 1582	. . . . . . . . . 10 ⊢ (∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k ))) ↔ ∃x ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
187	28, 186	bitri 240	. . . . . . . . 9 ⊢ (⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ∃x ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
188		exnal 1574	. . . . . . . . 9 ⊢ (∃x ¬ ((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m) ↔ ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
189	187, 188	bitri 240	. . . . . . . 8 ⊢ (⟪{a}, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ↔ ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
190	16, 189	bitri 240	. . . . . . 7 ⊢ (∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
191	190	exbii 1582	. . . . . 6 ⊢ (∃a∃t(t = {a} ∧ ⟪t, m⟫ ∈ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c)) ↔ ∃a ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
192	12, 191	bitri 240	. . . . 5 ⊢ (m ∈ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ∃a ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
193	192	notbii 287	. . . 4 ⊢ (¬ m ∈ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ¬ ∃a ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
194	1	elcompl 3226	. . . 4 ⊢ (m ∈ ∼ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ¬ m ∈ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c))
195		alex 1572	. . . 4 ⊢ (∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m) ↔ ¬ ∃a ¬ ∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
196	193, 194, 195	3bitr4i 268	. . 3 ⊢ (m ∈ ∼ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ↔ ∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m))
197	196	abbi2i 2465	. 2 ⊢ ∼ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) = {m ∣ ∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m)}
198		ssetkex 4295	. . . . . . . . . . . . . . . . . 18 ⊢ S_k ∈ V
199	198	sikex 4298	. . . . . . . . . . . . . . . . 17 ⊢ SI_k S_k ∈ V
200	199	sikex 4298	. . . . . . . . . . . . . . . 16 ⊢ SI_k SI_k S_k ∈ V
201	200	sikex 4298	. . . . . . . . . . . . . . 15 ⊢ SI_k SI_k SI_k S_k ∈ V
202	201	sikex 4298	. . . . . . . . . . . . . 14 ⊢ SI_k SI_k SI_k SI_k S_k ∈ V
203	202	sikex 4298	. . . . . . . . . . . . 13 ⊢ SI_k SI_k SI_k SI_k SI_k S_k ∈ V
204	203	ins3kex 4309	. . . . . . . . . . . 12 ⊢ Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ∈ V
205	199	ins3kex 4309	. . . . . . . . . . . . . . 15 ⊢ Ins3_k SI_k S_k ∈ V
206	205	ins2kex 4308	. . . . . . . . . . . . . 14 ⊢ Ins2_k Ins3_k SI_k S_k ∈ V
207		idkex 4315	. . . . . . . . . . . . . . 15 ⊢ I_k ∈ V
208	207	ins3kex 4309	. . . . . . . . . . . . . 14 ⊢ Ins3_k I_k ∈ V
209	206, 208	unex 4107	. . . . . . . . . . . . 13 ⊢ ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ∈ V
210	209	ins2kex 4308	. . . . . . . . . . . 12 ⊢ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k ) ∈ V
211	204, 210	symdifex 4109	. . . . . . . . . . 11 ⊢ ( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) ∈ V
212	149	pw1ex 4304	. . . . . . . . . . . . . . . . 17 ⊢ ℘₁1_c ∈ V
213	212	pw1ex 4304	. . . . . . . . . . . . . . . 16 ⊢ ℘₁℘₁1_c ∈ V
214	213	pw1ex 4304	. . . . . . . . . . . . . . 15 ⊢ ℘₁℘₁℘₁1_c ∈ V
215	214	pw1ex 4304	. . . . . . . . . . . . . 14 ⊢ ℘₁℘₁℘₁℘₁1_c ∈ V
216	215	pw1ex 4304	. . . . . . . . . . . . 13 ⊢ ℘₁℘₁℘₁℘₁℘₁1_c ∈ V
217	216	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘₁℘₁℘₁℘₁℘₁℘₁1_c ∈ V
218	217	pw1ex 4304	. . . . . . . . . . 11 ⊢ ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c ∈ V
219	211, 218	imakex 4301	. . . . . . . . . 10 ⊢ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∈ V
220	219	complex 4105	. . . . . . . . 9 ⊢ ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∈ V
221		addcexlem 4383	. . . . . . . . . . . . . . 15 ⊢ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ∈ V
222	221, 213	imakex 4301	. . . . . . . . . . . . . 14 ⊢ (( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
223	222	imagekex 4313	. . . . . . . . . . . . 13 ⊢ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
224	223	cnvkex 4288	. . . . . . . . . . . 12 ⊢ ^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
225	224, 198	cokex 4311	. . . . . . . . . . 11 ⊢ (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ∈ V
226	225	ins2kex 4308	. . . . . . . . . 10 ⊢ Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ∈ V
227	226	ins2kex 4308	. . . . . . . . 9 ⊢ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k ) ∈ V
228	220, 227	inex 4106	. . . . . . . 8 ⊢ ( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) ∈ V
229	228, 215	imakex 4301	. . . . . . 7 ⊢ (( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∈ V
230	229, 205	difex 4108	. . . . . 6 ⊢ ((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∈ V
231		vvex 4110	. . . . . . 7 ⊢ V ∈ V
232	231, 198	xpkex 4290	. . . . . 6 ⊢ (V ×_k S_k ) ∈ V
233	230, 232	difex 4108	. . . . 5 ⊢ (((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) ∈ V
234	233, 214	imakex 4301	. . . 4 ⊢ ((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) ∈ V
235	234, 149	imakex 4301	. . 3 ⊢ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ∈ V
236	235	complex 4105	. 2 ⊢ ∼ (((((( ∼ (( Ins3_k SI_k SI_k SI_k SI_k SI_k S_k ⊕ Ins2_k ( Ins2_k Ins3_k SI_k S_k ∪ Ins3_k I_k )) “_k ℘₁℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∩ Ins2_k Ins2_k (^◡_kImage_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∘_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ∖ Ins3_k SI_k S_k ) ∖ (V ×_k S_k )) “_k ℘₁℘₁℘₁1_c) “_k 1_c) ∈ V
237	197, 236	eqeltrri 2424	1 ⊢ {m ∣ ∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +_c 1_c)) → a ∈ m)} ∈ V

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 {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 ∘_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 I_k cidk 4185 +_c cplc 4376

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-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-pw 3725 df-sn 3742 df-pr 3743 df-opk 4059 df-1c 4137 df-pw1 4138 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-addc 4379

This theorem is referenced by: nnsucelr 4429

W3C validator