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

Theorem srelk 4524
 Description: Binary relationship form of the Sfin 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 ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (A, B))

Proof of Theorem srelk
Dummy variables t x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srelk.1 . . . . 5 A V
2 srelk.2 . . . . 5 B V
31, 2opkelxpk 4248 . . . 4 (⟪A, B ( Nn ×k Nn ) ↔ (A Nn B Nn ))
4 opkex 4113 . . . . . 6 A, B V
54elimak 4259 . . . . 5 (⟪A, B (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c) ↔ t 1 111ct, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)))
6 elpw131c 4149 . . . . . . . . 9 (t 1111cx t = {{{{x}}}})
76anbi1i 676 . . . . . . . 8 ((t 1111c t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ (x t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
8 19.41v 1901 . . . . . . . 8 (x(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ (x t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
97, 8bitr4i 243 . . . . . . 7 ((t 1111c t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ x(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
109exbii 1582 . . . . . 6 (t(t 1111c t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ tx(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
11 df-rex 2620 . . . . . 6 (t 1 111ct, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ t(t 1111c t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
12 excom 1741 . . . . . 6 (xt(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ tx(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
1310, 11, 123bitr4i 268 . . . . 5 (t 1 111ct, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ xt(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
14 snex 4111 . . . . . . . 8 {{{{x}}}} V
15 opkeq1 4059 . . . . . . . . 9 (t = {{{{x}}}} → ⟪t, ⟪A, B⟫⟫ = ⟪{{{{x}}}}, ⟪A, B⟫⟫)
1615eleq1d 2419 . . . . . . . 8 (t = {{{{x}}}} → (⟪t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))))
1714, 16ceqsexv 2894 . . . . . . 7 (t(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ ⟪{{{{x}}}}, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)))
18 elin 3219 . . . . . . 7 (⟪{{{{x}}}}, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ (⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)))
19 opkex 4113 . . . . . . . . . . 11 ⟪{{x}}, A V
2019elimak 4259 . . . . . . . . . 10 (⟪{{x}}, A (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
21 elpw121c 4148 . . . . . . . . . . . . . 14 (t 111cy t = {{{y}}})
2221anbi1i 676 . . . . . . . . . . . . 13 ((t 111c t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (y t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
23 19.41v 1901 . . . . . . . . . . . . 13 (y(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (y t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
2422, 23bitr4i 243 . . . . . . . . . . . 12 ((t 111c t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ y(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
2524exbii 1582 . . . . . . . . . . 11 (t(t 111c t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ty(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
26 df-rex 2620 . . . . . . . . . . 11 (t 1 11ct, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
27 excom 1741 . . . . . . . . . . 11 (yt(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ty(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
2825, 26, 273bitr4i 268 . . . . . . . . . 10 (t 1 11ct, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ yt(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
29 snex 4111 . . . . . . . . . . . . 13 {{{y}}} V
30 opkeq1 4059 . . . . . . . . . . . . . 14 (t = {{{y}}} → ⟪t, ⟪{{x}}, A⟫⟫ = ⟪{{{y}}}, ⟪{{x}}, A⟫⟫)
3130eleq1d 2419 . . . . . . . . . . . . 13 (t = {{{y}}} → (⟪t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
3229, 31ceqsexv 2894 . . . . . . . . . . . 12 (t(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
33 elin 3219 . . . . . . . . . . . 12 (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins2k Sk ))
34 snex 4111 . . . . . . . . . . . . . . 15 {y} V
35 snex 4111 . . . . . . . . . . . . . . 15 {{x}} V
3634, 35, 1otkelins3k 4256 . . . . . . . . . . . . . 14 (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪{y}, {{x}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
37 vex 2862 . . . . . . . . . . . . . . 15 y V
38 snex 4111 . . . . . . . . . . . . . . 15 {x} V
3937, 38opksnelsik 4265 . . . . . . . . . . . . . 14 (⟪{y}, {{x}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪y, {x}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
40 vex 2862 . . . . . . . . . . . . . . 15 x V
4137, 40eqpw1relk 4479 . . . . . . . . . . . . . 14 (⟪y, {x}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ y = 1x)
4236, 39, 413bitri 262 . . . . . . . . . . . . 13 (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ y = 1x)
4334, 35, 1otkelins2k 4255 . . . . . . . . . . . . . 14 (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins2k Sk ↔ ⟪{y}, A Sk )
4437, 1elssetk 4270 . . . . . . . . . . . . . 14 (⟪{y}, A Sky A)
4543, 44bitri 240 . . . . . . . . . . . . 13 (⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins2k Sky A)
4642, 45anbi12i 678 . . . . . . . . . . . 12 ((⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{y}}}, ⟪{{x}}, A⟫⟫ Ins2k Sk ) ↔ (y = 1x y A))
4732, 33, 463bitri 262 . . . . . . . . . . 11 (t(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (y = 1x y A))
4847exbii 1582 . . . . . . . . . 10 (yt(t = {{{y}}} t, ⟪{{x}}, A⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ y(y = 1x y A))
4920, 28, 483bitri 262 . . . . . . . . 9 (⟪{{x}}, A (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ y(y = 1x y A))
5035, 1, 2otkelins3k 4256 . . . . . . . . 9 (⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ ⟪{{x}}, A (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))
51 df-clel 2349 . . . . . . . . 9 (1x Ay(y = 1x y A))
5249, 50, 513bitr4i 268 . . . . . . . 8 (⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ 1x A)
53 opkex 4113 . . . . . . . . . . 11 ⟪{{x}}, B V
5453elimak 4259 . . . . . . . . . 10 (⟪{{x}}, B (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ))
5521anbi1i 676 . . . . . . . . . . . . 13 ((t 111c t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ (y t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
56 19.41v 1901 . . . . . . . . . . . . 13 (y(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ (y t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
5755, 56bitr4i 243 . . . . . . . . . . . 12 ((t 111c t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ y(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
5857exbii 1582 . . . . . . . . . . 11 (t(t 111c t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ ty(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
59 df-rex 2620 . . . . . . . . . . 11 (t 1 11ct, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
60 excom 1741 . . . . . . . . . . 11 (yt(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ ty(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
6158, 59, 603bitr4i 268 . . . . . . . . . 10 (t 1 11ct, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) ↔ yt(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
62 opkeq1 4059 . . . . . . . . . . . . . 14 (t = {{{y}}} → ⟪t, ⟪{{x}}, B⟫⟫ = ⟪{{{y}}}, ⟪{{x}}, B⟫⟫)
6362eleq1d 2419 . . . . . . . . . . . . 13 (t = {{{y}}} → (⟪t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) ↔ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )))
6429, 63ceqsexv 2894 . . . . . . . . . . . 12 (t(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ))
65 elin 3219 . . . . . . . . . . . 12 (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) ↔ (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins2k Sk ))
6634, 35, 2otkelins3k 4256 . . . . . . . . . . . . . 14 (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ ⟪{y}, {{x}}⟫ SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c))
6737, 38opksnelsik 4265 . . . . . . . . . . . . . 14 (⟪{y}, {{x}}⟫ SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ ⟪y, {x}⟫ ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c))
68 opkex 4113 . . . . . . . . . . . . . . . . . . 19 y, {x}⟫ V
6968elimak 4259 . . . . . . . . . . . . . . . . . 18 (⟪y, {x}⟫ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ t 1 11ct, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ))
70 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . 22 (t 111cz t = {{{z}}})
7170anbi1i 676 . . . . . . . . . . . . . . . . . . . . 21 ((t 111c t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ (z t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
72 19.41v 1901 . . . . . . . . . . . . . . . . . . . . 21 (z(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ (z t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
7371, 72bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 ((t 111c t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ z(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
7473exbii 1582 . . . . . . . . . . . . . . . . . . 19 (t(t 111c t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ tz(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
75 df-rex 2620 . . . . . . . . . . . . . . . . . . 19 (t 1 11ct, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ t(t 111c t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
76 excom 1741 . . . . . . . . . . . . . . . . . . 19 (zt(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ tz(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
7774, 75, 763bitr4i 268 . . . . . . . . . . . . . . . . . 18 (t 1 11ct, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ zt(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
78 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{{z}}} V
79 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{{z}}} → ⟪t, ⟪y, {x}⟫⟫ = ⟪{{{z}}}, ⟪y, {x}⟫⟫)
8079eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (t = {{{z}}} → (⟪t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )))
8178, 80ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ))
82 elsymdif 3223 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{z}}}, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk ) ↔ ¬ (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins3k Sk ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins2k SIk Sk ))
83 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {z} V
8483, 37, 38otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins3k Sk ↔ ⟪{z}, y Sk )
85 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 z V
8685, 37elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{z}, y Skz y)
8784, 86bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins3k Skz y)
8883, 37, 38otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins2k SIk Sk ↔ ⟪{z}, {x}⟫ SIk Sk )
8985, 40opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{z}, {x}⟫ SIk Sk ↔ ⟪z, x Sk )
90 opkelssetkg 4268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((z V x V) → (⟪z, x Skz x))
9185, 40, 90mp2an 653 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪z, x Skz x)
9288, 89, 913bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins2k SIk Skz x)
9387, 92bibi12i 306 . . . . . . . . . . . . . . . . . . . . 21 ((⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins3k Sk ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins2k SIk Sk ) ↔ (z yz x))
9493notbii 287 . . . . . . . . . . . . . . . . . . . 20 (¬ (⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins3k Sk ↔ ⟪{{{z}}}, ⟪y, {x}⟫⟫ Ins2k SIk Sk ) ↔ ¬ (z yz x))
9581, 82, 943bitri 262 . . . . . . . . . . . . . . . . . . 19 (t(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ ¬ (z yz x))
9695exbii 1582 . . . . . . . . . . . . . . . . . 18 (zt(t = {{{z}}} t, ⟪y, {x}⟫⟫ ( Ins3k SkIns2k SIk Sk )) ↔ z ¬ (z yz x))
9769, 77, 963bitri 262 . . . . . . . . . . . . . . . . 17 (⟪y, {x}⟫ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ z ¬ (z yz x))
9897notbii 287 . . . . . . . . . . . . . . . 16 (¬ ⟪y, {x}⟫ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ ¬ z ¬ (z yz x))
9968elcompl 3225 . . . . . . . . . . . . . . . 16 (⟪y, {x}⟫ ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ ¬ ⟪y, {x}⟫ (( Ins3k SkIns2k SIk Sk ) “k 111c))
100 alex 1572 . . . . . . . . . . . . . . . 16 (z(z yz x) ↔ ¬ z ¬ (z yz x))
10198, 99, 1003bitr4i 268 . . . . . . . . . . . . . . 15 (⟪y, {x}⟫ ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ z(z yz x))
102 df-pw 3724 . . . . . . . . . . . . . . . . 17 x = {z z x}
103102eqeq2i 2363 . . . . . . . . . . . . . . . 16 (y = xy = {z z x})
104 abeq2 2458 . . . . . . . . . . . . . . . 16 (y = {z z x} ↔ z(z yz x))
105103, 104bitri 240 . . . . . . . . . . . . . . 15 (y = xz(z yz x))
106101, 105bitr4i 243 . . . . . . . . . . . . . 14 (⟪y, {x}⟫ ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ y = x)
10766, 67, 1063bitri 262 . . . . . . . . . . . . 13 (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ↔ y = x)
10834, 35, 2otkelins2k 4255 . . . . . . . . . . . . . 14 (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins2k Sk ↔ ⟪{y}, B Sk )
10937, 2elssetk 4270 . . . . . . . . . . . . . 14 (⟪{y}, B Sky B)
110108, 109bitri 240 . . . . . . . . . . . . 13 (⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins2k Sky B)
111107, 110anbi12i 678 . . . . . . . . . . . 12 ((⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ⟪{{{y}}}, ⟪{{x}}, B⟫⟫ Ins2k Sk ) ↔ (y = x y B))
11264, 65, 1113bitri 262 . . . . . . . . . . 11 (t(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ (y = x y B))
113112exbii 1582 . . . . . . . . . 10 (yt(t = {{{y}}} t, ⟪{{x}}, B⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk )) ↔ y(y = x y B))
11454, 61, 1133bitri 262 . . . . . . . . 9 (⟪{{x}}, B (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ y(y = x y B))
11535, 1, 2otkelins2k 4255 . . . . . . . . 9 (⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ ⟪{{x}}, B (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))
116 df-clel 2349 . . . . . . . . 9 (x By(y = x y B))
117114, 115, 1163bitr4i 268 . . . . . . . 8 (⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ x B)
11852, 117anbi12i 678 . . . . . . 7 ((⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ⟪{{{{x}}}}, ⟪A, B⟫⟫ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ (1x A x B))
11917, 18, 1183bitri 262 . . . . . 6 (t(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ (1x A x B))
120119exbii 1582 . . . . 5 (xt(t = {{{{x}}}} t, ⟪A, B⟫⟫ ( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ x(1x A x B))
1215, 13, 1203bitri 262 . . . 4 (⟪A, B (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c) ↔ x(1x A x B))
1223, 121anbi12i 678 . . 3 ((⟪A, B ( Nn ×k Nn ) A, B (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ((A Nn B Nn ) x(1x A x B)))
123 df-3an 936 . . 3 ((A Nn B Nn x(1x A x B)) ↔ ((A Nn B Nn ) x(1x A x B)))
124122, 123bitr4i 243 . 2 ((⟪A, B ( Nn ×k Nn ) A, B (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ (A Nn B Nn x(1x A x B)))
125 elin 3219 . 2 (⟪A, B (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ (⟪A, B ( Nn ×k Nn ) A, B (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
126 df-sfin 4446 . 2 ( Sfin (A, B) ↔ (A Nn B Nn x(1x A x B)))
127124, 125, 1263bitr4i 268 1 (⟪A, B (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (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 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209   ⊆ wss 3257  ℘cpw 3722  {csn 3737  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373   Sfin wsfin 4438 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 4078  ax-sn 4087 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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-pw 3724  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-sik 4192  df-ssetk 4193  df-sfin 4446 This theorem is referenced by:  sfintfinlem1  4531  spfinex  4537
 Copyright terms: Public domain W3C validator