srelk - New Foundations Explorer

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

Theorem srelk 4525

Description: Binary relationship form of the S_fin relationship. (Contributed by SF, 23-Jan-2015.)

**Hypotheses**
Ref	Expression
srelk.1	⊢ A ∈ V
srelk.2	⊢ B ∈ V

**Assertion**
Ref	Expression
srelk	⊢ (⟪A, B⟫ ∈ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ S_fin (A, B))

Proof of Theorem srelk Dummy variables t x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		srelk.1	. . . . 5 ⊢ A ∈ V
2		srelk.2	. . . . 5 ⊢ B ∈ V
3	1, 2	opkelxpk 4249	. . . 4 ⊢ (⟪A, B⟫ ∈ ( Nn ×_k Nn ) ↔ (A ∈ Nn ∧ B ∈ Nn ))
4		opkex 4114	. . . . . 6 ⊢ ⟪A, B⟫ ∈ V
5	4	elimak 4260	. . . . 5 ⊢ (⟪A, B⟫ ∈ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
6		elpw131c 4150	. . . . . . . . 9 ⊢ (t ∈ ℘₁℘₁℘₁1_c ↔ ∃x t = {{{{x}}}})
7	6	anbi1i 676	. . . . . . . 8 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (∃x t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
8		19.41v 1901	. . . . . . . 8 ⊢ (∃x(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (∃x t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
9	7, 8	bitr4i 243	. . . . . . 7 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃x(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
10	9	exbii 1582	. . . . . 6 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
11		df-rex 2621	. . . . . 6 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
12		excom 1741	. . . . . 6 ⊢ (∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
13	10, 11, 12	3bitr4i 268	. . . . 5 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
14		snex 4112	. . . . . . . 8 ⊢ {{{{x}}}} ∈ V
15		opkeq1 4060	. . . . . . . . 9 ⊢ (t = {{{{x}}}} → ⟪t, ⟪A, B⟫⟫ = ⟪{{{{x}}}}, ⟪A, B⟫⟫)
16	15	eleq1d 2419	. . . . . . . 8 ⊢ (t = {{{{x}}}} → (⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
17	14, 16	ceqsexv 2895	. . . . . . 7 ⊢ (∃t(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
18		elin 3220	. . . . . . 7 ⊢ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
19		opkex 4114	. . . . . . . . . . 11 ⊢ ⟪{{x}}, A⟫ ∈ V
20	19	elimak 4260	. . . . . . . . . 10 ⊢ (⟪{{x}}, A⟫ ∈ (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ))
21		elpw121c 4149	. . . . . . . . . . . . . 14 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃y t = {{{y}}})
22	21	anbi1i 676	. . . . . . . . . . . . 13 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ (∃y t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
23		19.41v 1901	. . . . . . . . . . . . 13 ⊢ (∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ (∃y t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
24	22, 23	bitr4i 243	. . . . . . . . . . . 12 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ ∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
25	24	exbii 1582	. . . . . . . . . . 11 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ ∃t∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
26		df-rex 2621	. . . . . . . . . . 11 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
27		excom 1741	. . . . . . . . . . 11 ⊢ (∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ ∃t∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
28	25, 26, 27	3bitr4i 268	. . . . . . . . . 10 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) ↔ ∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
29		snex 4112	. . . . . . . . . . . . 13 ⊢ {{{y}}} ∈ V
30		opkeq1 4060	. . . . . . . . . . . . . 14 ⊢ (t = {{{y}}} → ⟪t, ⟪{{x}}, A⟫⟫ = ⟪{{{y}}}, ⟪{{x}}, A⟫⟫)
31	30	eleq1d 2419	. . . . . . . . . . . . 13 ⊢ (t = {{{y}}} → (⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) ↔ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )))
32	29, 31	ceqsexv 2895	. . . . . . . . . . . 12 ⊢ (∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ))
33		elin 3220	. . . . . . . . . . . 12 ⊢ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) ↔ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins2_k S_k ))
34		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {y} ∈ V
35		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {{x}} ∈ V
36	34, 35, 1	otkelins3k 4257	. . . . . . . . . . . . . 14 ⊢ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{y}, {{x}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
37		vex 2863	. . . . . . . . . . . . . . 15 ⊢ y ∈ V
38		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {x} ∈ V
39	37, 38	opksnelsik 4266	. . . . . . . . . . . . . 14 ⊢ (⟪{y}, {{x}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪y, {x}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
40		vex 2863	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
41	37, 40	eqpw1relk 4480	. . . . . . . . . . . . . 14 ⊢ (⟪y, {x}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ y = ℘₁x)
42	36, 39, 41	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ y = ℘₁x)
43	34, 35, 1	otkelins2k 4256	. . . . . . . . . . . . . 14 ⊢ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins2_k S_k ↔ ⟪{y}, A⟫ ∈ S_k )
44	37, 1	elssetk 4271	. . . . . . . . . . . . . 14 ⊢ (⟪{y}, A⟫ ∈ S_k ↔ y ∈ A)
45	43, 44	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins2_k S_k ↔ y ∈ A)
46	42, 45	anbi12i 678	. . . . . . . . . . . 12 ⊢ ((⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ∈ Ins2_k S_k ) ↔ (y = ℘₁x ∧ y ∈ A))
47	32, 33, 46	3bitri 262	. . . . . . . . . . 11 ⊢ (∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ (y = ℘₁x ∧ y ∈ A))
48	47	exbii 1582	. . . . . . . . . 10 ⊢ (∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, A⟫⟫ ∈ ( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k )) ↔ ∃y(y = ℘₁x ∧ y ∈ A))
49	20, 28, 48	3bitri 262	. . . . . . . . 9 ⊢ (⟪{{x}}, A⟫ ∈ (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃y(y = ℘₁x ∧ y ∈ A))
50	35, 1, 2	otkelins3k 4257	. . . . . . . . 9 ⊢ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{{x}}, A⟫ ∈ (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
51		df-clel 2349	. . . . . . . . 9 ⊢ (℘₁x ∈ A ↔ ∃y(y = ℘₁x ∧ y ∈ A))
52	49, 50, 51	3bitr4i 268	. . . . . . . 8 ⊢ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ℘₁x ∈ A)
53		opkex 4114	. . . . . . . . . . 11 ⊢ ⟪{{x}}, B⟫ ∈ V
54	53	elimak 4260	. . . . . . . . . 10 ⊢ (⟪{{x}}, B⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ))
55	21	anbi1i 676	. . . . . . . . . . . . 13 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (∃y t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
56		19.41v 1901	. . . . . . . . . . . . 13 ⊢ (∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (∃y t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
57	55, 56	bitr4i 243	. . . . . . . . . . . 12 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
58	57	exbii 1582	. . . . . . . . . . 11 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃t∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
59		df-rex 2621	. . . . . . . . . . 11 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
60		excom 1741	. . . . . . . . . . 11 ⊢ (∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃t∃y(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
61	58, 59, 60	3bitr4i 268	. . . . . . . . . 10 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
62		opkeq1 4060	. . . . . . . . . . . . . 14 ⊢ (t = {{{y}}} → ⟪t, ⟪{{x}}, B⟫⟫ = ⟪{{{y}}}, ⟪{{x}}, B⟫⟫)
63	62	eleq1d 2419	. . . . . . . . . . . . 13 ⊢ (t = {{{y}}} → (⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
64	29, 63	ceqsexv 2895	. . . . . . . . . . . 12 ⊢ (∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ))
65		elin 3220	. . . . . . . . . . . 12 ⊢ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins2_k S_k ))
66	34, 35, 2	otkelins3k 4257	. . . . . . . . . . . . . 14 ⊢ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{y}, {{x}}⟫ ∈ SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c))
67	37, 38	opksnelsik 4266	. . . . . . . . . . . . . 14 ⊢ (⟪{y}, {{x}}⟫ ∈ SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪y, {x}⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c))
68		opkex 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟪y, {x}⟫ ∈ V
69	68	elimak 4260	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪y, {x}⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ))
70		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃z t = {{{z}}})
71	70	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
72		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
73	71, 72	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
74	73	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
75		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
76		excom 1741	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
77	74, 75, 76	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
78		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {{{z}}} ∈ V
79		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = {{{z}}} → ⟪t, ⟪y, {x}⟫⟫ = ⟪{{{z}}}, ⟪y, {x}⟫⟫)
80	79	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = {{{z}}} → (⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )))
81	78, 80	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ))
82		elsymdif 3224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) ↔ ¬ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins2_k SI_k S_k ))
83		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {z} ∈ V
84	83, 37, 38	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{z}, y⟫ ∈ S_k )
85		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ z ∈ V
86	85, 37	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{z}, y⟫ ∈ S_k ↔ z ∈ y)
87	84, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins3_k S_k ↔ z ∈ y)
88	83, 37, 38	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins2_k SI_k S_k ↔ ⟪{z}, {x}⟫ ∈ SI_k S_k )
89	85, 40	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{z}, {x}⟫ ∈ SI_k S_k ↔ ⟪z, x⟫ ∈ S_k )
90		opkelssetkg 4269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((z ∈ V ∧ x ∈ V) → (⟪z, x⟫ ∈ S_k ↔ z ⊆ x))
91	85, 40, 90	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪z, x⟫ ∈ S_k ↔ z ⊆ x)
92	88, 89, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins2_k SI_k S_k ↔ z ⊆ x)
93	87, 92	bibi12i 306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins2_k SI_k S_k ) ↔ (z ∈ y ↔ z ⊆ x))
94	93	notbii 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ∈ Ins2_k SI_k S_k ) ↔ ¬ (z ∈ y ↔ z ⊆ x))
95	81, 82, 94	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ¬ (z ∈ y ↔ z ⊆ x))
96	95	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪y, {x}⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k )) ↔ ∃z ¬ (z ∈ y ↔ z ⊆ x))
97	69, 77, 96	3bitri 262	. . . . . . . . . . . . . . . . 17 ⊢ (⟪y, {x}⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃z ¬ (z ∈ y ↔ z ⊆ x))
98	97	notbii 287	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟪y, {x}⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ ∃z ¬ (z ∈ y ↔ z ⊆ x))
99	68	elcompl 3226	. . . . . . . . . . . . . . . 16 ⊢ (⟪y, {x}⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ ⟪y, {x}⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c))
100		alex 1572	. . . . . . . . . . . . . . . 16 ⊢ (∀z(z ∈ y ↔ z ⊆ x) ↔ ¬ ∃z ¬ (z ∈ y ↔ z ⊆ x))
101	98, 99, 100	3bitr4i 268	. . . . . . . . . . . . . . 15 ⊢ (⟪y, {x}⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ ∀z(z ∈ y ↔ z ⊆ x))
102		df-pw 3725	. . . . . . . . . . . . . . . . 17 ⊢ ℘x = {z ∣ z ⊆ x}
103	102	eqeq2i 2363	. . . . . . . . . . . . . . . 16 ⊢ (y = ℘x ↔ y = {z ∣ z ⊆ x})
104		abeq2 2459	. . . . . . . . . . . . . . . 16 ⊢ (y = {z ∣ z ⊆ x} ↔ ∀z(z ∈ y ↔ z ⊆ x))
105	103, 104	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (y = ℘x ↔ ∀z(z ∈ y ↔ z ⊆ x))
106	101, 105	bitr4i 243	. . . . . . . . . . . . . 14 ⊢ (⟪y, {x}⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ y = ℘x)
107	66, 67, 106	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ↔ y = ℘x)
108	34, 35, 2	otkelins2k 4256	. . . . . . . . . . . . . 14 ⊢ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins2_k S_k ↔ ⟪{y}, B⟫ ∈ S_k )
109	37, 2	elssetk 4271	. . . . . . . . . . . . . 14 ⊢ (⟪{y}, B⟫ ∈ S_k ↔ y ∈ B)
110	108, 109	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins2_k S_k ↔ y ∈ B)
111	107, 110	anbi12i 678	. . . . . . . . . . . 12 ⊢ ((⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ∈ Ins2_k S_k ) ↔ (y = ℘x ∧ y ∈ B))
112	64, 65, 111	3bitri 262	. . . . . . . . . . 11 ⊢ (∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (y = ℘x ∧ y ∈ B))
113	112	exbii 1582	. . . . . . . . . 10 ⊢ (∃y∃t(t = {{{y}}} ∧ ⟪t, ⟪{{x}}, B⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃y(y = ℘x ∧ y ∈ B))
114	54, 61, 113	3bitri 262	. . . . . . . . 9 ⊢ (⟪{{x}}, B⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃y(y = ℘x ∧ y ∈ B))
115	35, 1, 2	otkelins2k 4256	. . . . . . . . 9 ⊢ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪{{x}}, B⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
116		df-clel 2349	. . . . . . . . 9 ⊢ (℘x ∈ B ↔ ∃y(y = ℘x ∧ y ∈ B))
117	114, 115, 116	3bitr4i 268	. . . . . . . 8 ⊢ (⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ℘x ∈ B)
118	52, 117	anbi12i 678	. . . . . . 7 ⊢ ((⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ∈ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (℘₁x ∈ A ∧ ℘x ∈ B))
119	17, 18, 118	3bitri 262	. . . . . 6 ⊢ (∃t(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (℘₁x ∈ A ∧ ℘x ∈ B))
120	119	exbii 1582	. . . . 5 ⊢ (∃x∃t(t = {{{{x}}}} ∧ ⟪t, ⟪A, B⟫⟫ ∈ ( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃x(℘₁x ∈ A ∧ ℘x ∈ B))
121	5, 13, 120	3bitri 262	. . . 4 ⊢ (⟪A, B⟫ ∈ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ↔ ∃x(℘₁x ∈ A ∧ ℘x ∈ B))
122	3, 121	anbi12i 678	. . 3 ⊢ ((⟪A, B⟫ ∈ ( Nn ×_k Nn ) ∧ ⟪A, B⟫ ∈ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ((A ∈ Nn ∧ B ∈ Nn ) ∧ ∃x(℘₁x ∈ A ∧ ℘x ∈ B)))
123		df-3an 936	. . 3 ⊢ ((A ∈ Nn ∧ B ∈ Nn ∧ ∃x(℘₁x ∈ A ∧ ℘x ∈ B)) ↔ ((A ∈ Nn ∧ B ∈ Nn ) ∧ ∃x(℘₁x ∈ A ∧ ℘x ∈ B)))
124	122, 123	bitr4i 243	. 2 ⊢ ((⟪A, B⟫ ∈ ( Nn ×_k Nn ) ∧ ⟪A, B⟫ ∈ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ (A ∈ Nn ∧ B ∈ Nn ∧ ∃x(℘₁x ∈ A ∧ ℘x ∈ B)))
125		elin 3220	. 2 ⊢ (⟪A, B⟫ ∈ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ (⟪A, B⟫ ∈ ( Nn ×_k Nn ) ∧ ⟪A, B⟫ ∈ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
126		df-sfin 4447	. 2 ⊢ ( S_fin (A, B) ↔ (A ∈ Nn ∧ B ∈ Nn ∧ ∃x(℘₁x ∈ A ∧ ℘x ∈ B)))
127	124, 125, 126	3bitr4i 268	1 ⊢ (⟪A, B⟫ ∈ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ S_fin (A, B))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176 ∧ wa 358 ∧ w3a 934 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∩ cin 3209 ⊕ csymdif 3210 ⊆ wss 3258 ℘cpw 3723 {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 S_fin wsfin 4439

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-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-ins2k 4188 df-ins3k 4189 df-imak 4190 df-sik 4193 df-ssetk 4194 df-sfin 4447

This theorem is referenced by: sfintfinlem1 4532 spfinex 4538

W3C validator