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

Theorem nnpweqlem1 4522
 Description: Lemma for nnpweq 4523. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
Assertion
Ref Expression
nnpweqlem1 {m a m b m n Nn (a n b n)} V
Distinct variable group:   m,a,b,n

Proof of Theorem nnpweqlem1
Dummy variables t x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . 5 m V
21eluni1 4173 . . . 4 (m 1 ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ {m} ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c))
3 snex 4111 . . . . . . . . . 10 {{a}} V
4 opkeq1 4059 . . . . . . . . . . 11 (t = {{a}} → ⟪t, {m}⟫ = ⟪{{a}}, {m}⟫)
54eleq1d 2419 . . . . . . . . . 10 (t = {{a}} → (⟪t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) ↔ ⟪{{a}}, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
63, 5ceqsexv 2894 . . . . . . . . 9 (t(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ ⟪{{a}}, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)))
7 elin 3219 . . . . . . . . 9 (⟪{{a}}, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) ↔ (⟪{{a}}, {m}⟫ SIk Sk ⟪{{a}}, {m}⟫ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)))
8 snex 4111 . . . . . . . . . . . 12 {a} V
98, 1opksnelsik 4265 . . . . . . . . . . 11 (⟪{{a}}, {m}⟫ SIk Sk ↔ ⟪{a}, m Sk )
10 vex 2862 . . . . . . . . . . . 12 a V
1110, 1elssetk 4270 . . . . . . . . . . 11 (⟪{a}, m Ska m)
129, 11bitri 240 . . . . . . . . . 10 (⟪{{a}}, {m}⟫ SIk Ska m)
13 opkex 4113 . . . . . . . . . . . . 13 ⟪{{a}}, {m}⟫ V
1413elimak 4259 . . . . . . . . . . . 12 (⟪{{a}}, {m}⟫ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c) ↔ t 1 111ct, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )))
15 elpw131c 4149 . . . . . . . . . . . . . . . 16 (t 1111cb t = {{{{b}}}})
1615anbi1i 676 . . . . . . . . . . . . . . 15 ((t 1111c t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ (b t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
17 19.41v 1901 . . . . . . . . . . . . . . 15 (b(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ (b t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
1816, 17bitr4i 243 . . . . . . . . . . . . . 14 ((t 1111c t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ b(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
1918exbii 1582 . . . . . . . . . . . . 13 (t(t 1111c t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ tb(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
20 df-rex 2620 . . . . . . . . . . . . 13 (t 1 111ct, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) ↔ t(t 1111c t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
21 excom 1741 . . . . . . . . . . . . 13 (bt(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ tb(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
2219, 20, 213bitr4i 268 . . . . . . . . . . . 12 (t 1 111ct, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) ↔ bt(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
23 snex 4111 . . . . . . . . . . . . . . 15 {{{{b}}}} V
24 opkeq1 4059 . . . . . . . . . . . . . . . 16 (t = {{{{b}}}} → ⟪t, ⟪{{a}}, {m}⟫⟫ = ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫)
2524eleq1d 2419 . . . . . . . . . . . . . . 15 (t = {{{{b}}}} → (⟪t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) ↔ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))))
2623, 25ceqsexv 2894 . . . . . . . . . . . . . 14 (t(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )))
27 eldif 3221 . . . . . . . . . . . . . 14 (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) ↔ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins2k SIk Sk ¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )))
28 snex 4111 . . . . . . . . . . . . . . . . 17 {{b}} V
29 snex 4111 . . . . . . . . . . . . . . . . 17 {m} V
3028, 3, 29otkelins2k 4255 . . . . . . . . . . . . . . . 16 (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins2k SIk Sk ↔ ⟪{{b}}, {m}⟫ SIk Sk )
31 snex 4111 . . . . . . . . . . . . . . . . 17 {b} V
3231, 1opksnelsik 4265 . . . . . . . . . . . . . . . 16 (⟪{{b}}, {m}⟫ SIk Sk ↔ ⟪{b}, m Sk )
33 vex 2862 . . . . . . . . . . . . . . . . 17 b V
3433, 1elssetk 4270 . . . . . . . . . . . . . . . 16 (⟪{b}, m Skb m)
3530, 32, 343bitri 262 . . . . . . . . . . . . . . 15 (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins2k SIk Skb m)
3628, 3, 29otkelins3k 4256 . . . . . . . . . . . . . . . . 17 (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) ↔ ⟪{{b}}, {{a}}⟫ (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))
37 opkex 4113 . . . . . . . . . . . . . . . . . . 19 ⟪{{b}}, {{a}}⟫ V
3837elimak 4259 . . . . . . . . . . . . . . . . . 18 (⟪{{b}}, {{a}}⟫ (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) ↔ t 1 1 Nnt, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)))
39 elpw12 4145 . . . . . . . . . . . . . . . . . . . . . 22 (t 11 Nnn Nn t = {{n}})
4039anbi1i 676 . . . . . . . . . . . . . . . . . . . . 21 ((t 11 Nn t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (n Nn t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
41 r19.41v 2764 . . . . . . . . . . . . . . . . . . . . 21 (n Nn (t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (n Nn t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
4240, 41bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 ((t 11 Nn t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ n Nn (t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
4342exbii 1582 . . . . . . . . . . . . . . . . . . 19 (t(t 11 Nn t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ tn Nn (t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
44 df-rex 2620 . . . . . . . . . . . . . . . . . . 19 (t 1 1 Nnt, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ t(t 11 Nn t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
45 rexcom4 2878 . . . . . . . . . . . . . . . . . . 19 (n Nn t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ tn Nn (t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
4643, 44, 453bitr4i 268 . . . . . . . . . . . . . . . . . 18 (t 1 1 Nnt, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ n Nn t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
4738, 46bitri 240 . . . . . . . . . . . . . . . . 17 (⟪{{b}}, {{a}}⟫ (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) ↔ n Nn t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
48 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {{n}} V
49 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . 21 (t = {{n}} → ⟪t, ⟪{{b}}, {{a}}⟫⟫ = ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫)
5049eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (t = {{n}} → (⟪t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))))
5148, 50ceqsexv 2894 . . . . . . . . . . . . . . . . . . 19 (t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)))
52 elin 3219 . . . . . . . . . . . . . . . . . . 19 (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)))
53 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . 23 n, {{a}}⟫ V
5453elimak 4259 . . . . . . . . . . . . . . . . . . . . . 22 (⟪n, {{a}}⟫ (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ t 1 11ct, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ))
55 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t 111cx t = {{{x}}})
5655anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((t 111c t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
57 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
5856, 57bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 111c t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ x(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
5958exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t 111c t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ tx(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
60 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (t 1 11ct, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ t(t 111c t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
61 excom 1741 . . . . . . . . . . . . . . . . . . . . . . 23 (xt(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ tx(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
6259, 60, 613bitr4i 268 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 11ct, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ xt(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
63 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25 {{{x}}} V
64 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t = {{{x}}} → ⟪t, ⟪n, {{a}}⟫⟫ = ⟪{{{x}}}, ⟪n, {{a}}⟫⟫)
6564eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{{x}}} → (⟪t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
6663, 65ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 (t(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ))
67 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins3k Sk ))
68 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {x} V
69 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 n V
7068, 69, 3otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪{x}, {{a}}⟫ SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
71 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 x V
7271, 8opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{x}, {{a}}⟫ SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪x, {a}⟫ k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
7371, 8opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪x, {a}⟫ k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪{a}, x ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
7410, 71eqpwrelk 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{a}, x ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = a)
7573, 74bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪x, {a}⟫ k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = a)
7670, 72, 753bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = a)
7768, 69, 3otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins3k Sk ↔ ⟪{x}, n Sk )
7871, 69elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{x}, n Skx n)
7977, 78bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins3k Skx n)
8076, 79anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ Ins3k Sk ) ↔ (x = a x n))
8166, 67, 803bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x = a x n))
8281exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (xt(t = {{{x}}} t, ⟪n, {{a}}⟫⟫ ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ x(x = a x n))
8354, 62, 823bitri 262 . . . . . . . . . . . . . . . . . . . . 21 (⟪n, {{a}}⟫ (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ x(x = a x n))
8469, 28, 3otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ ⟪n, {{a}}⟫ (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))
85 df-clel 2349 . . . . . . . . . . . . . . . . . . . . 21 (a nx(x = a x n))
8683, 84, 853bitr4i 268 . . . . . . . . . . . . . . . . . . . 20 (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ a n)
87 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . 23 n, {{b}}⟫ V
8887elimak 4259 . . . . . . . . . . . . . . . . . . . . . 22 (⟪n, {{b}}⟫ (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ t 1 11ct, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ))
8955anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((t 111c t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
90 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
9189, 90bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 111c t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ x(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
9291exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t 111c t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ tx(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
93 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (t 1 11ct, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ t(t 111c t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
94 excom 1741 . . . . . . . . . . . . . . . . . . . . . . 23 (xt(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ tx(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
9592, 93, 943bitr4i 268 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 11ct, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ xt(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
96 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t = {{{x}}} → ⟪t, ⟪n, {{b}}⟫⟫ = ⟪{{{x}}}, ⟪n, {{b}}⟫⟫)
9796eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{{x}}} → (⟪t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )))
9863, 97ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 (t(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ))
99 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) ↔ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins3k Sk ))
10068, 69, 28otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪{x}, {{b}}⟫ k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
10168, 28opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{x}, {{b}}⟫ k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪{{b}}, {x}⟫ SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
10231, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{b}}, {x}⟫ SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ ⟪{b}, x ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c))
10333, 71eqpwrelk 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{b}, x ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = b)
104102, 103bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{b}}, {x}⟫ SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = b)
105100, 101, 1043bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ x = b)
10668, 69, 28otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins3k Sk ↔ ⟪{x}, n Sk )
107106, 78bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins3k Skx n)
108105, 107anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ Ins3k Sk ) ↔ (x = b x n))
10998, 99, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ (x = b x n))
110109exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (xt(t = {{{x}}} t, ⟪n, {{b}}⟫⟫ ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk )) ↔ x(x = b x n))
11188, 95, 1103bitri 262 . . . . . . . . . . . . . . . . . . . . 21 (⟪n, {{b}}⟫ (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ x(x = b x n))
11269, 28, 3otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ ⟪n, {{b}}⟫ (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))
113 df-clel 2349 . . . . . . . . . . . . . . . . . . . . 21 (b nx(x = b x n))
114111, 112, 1133bitr4i 268 . . . . . . . . . . . . . . . . . . . 20 (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ b n)
11586, 114anbi12i 678 . . . . . . . . . . . . . . . . . . 19 ((⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ (a n b n))
11651, 52, 1153bitri 262 . . . . . . . . . . . . . . . . . 18 (t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (a n b n))
117116rexbii 2639 . . . . . . . . . . . . . . . . 17 (n Nn t(t = {{n}} t, ⟪{{b}}, {{a}}⟫⟫ ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ n Nn (a n b n))
11836, 47, 1173bitri 262 . . . . . . . . . . . . . . . 16 (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) ↔ n Nn (a n b n))
119118notbii 287 . . . . . . . . . . . . . . 15 (¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) ↔ ¬ n Nn (a n b n))
12035, 119anbi12i 678 . . . . . . . . . . . . . 14 ((⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins2k SIk Sk ¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) ↔ (b m ¬ n Nn (a n b n)))
12126, 27, 1203bitri 262 . . . . . . . . . . . . 13 (t(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ (b m ¬ n Nn (a n b n)))
122121exbii 1582 . . . . . . . . . . . 12 (bt(t = {{{{b}}}} t, ⟪{{a}}, {m}⟫⟫ ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ))) ↔ b(b m ¬ n Nn (a n b n)))
12314, 22, 1223bitri 262 . . . . . . . . . . 11 (⟪{{a}}, {m}⟫ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c) ↔ b(b m ¬ n Nn (a n b n)))
124 df-rex 2620 . . . . . . . . . . 11 (b m ¬ n Nn (a n b n) ↔ b(b m ¬ n Nn (a n b n)))
125 rexnal 2625 . . . . . . . . . . 11 (b m ¬ n Nn (a n b n) ↔ ¬ b m n Nn (a n b n))
126123, 124, 1253bitr2i 264 . . . . . . . . . 10 (⟪{{a}}, {m}⟫ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c) ↔ ¬ b m n Nn (a n b n))
12712, 126anbi12i 678 . . . . . . . . 9 ((⟪{{a}}, {m}⟫ SIk Sk ⟪{{a}}, {m}⟫ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) ↔ (a m ¬ b m n Nn (a n b n)))
1286, 7, 1273bitri 262 . . . . . . . 8 (t(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ (a m ¬ b m n Nn (a n b n)))
129128exbii 1582 . . . . . . 7 (at(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ a(a m ¬ b m n Nn (a n b n)))
13029elimak 4259 . . . . . . . 8 ({m} (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ t 1 1ct, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)))
131 elpw11c 4147 . . . . . . . . . . . 12 (t 11ca t = {{a}})
132131anbi1i 676 . . . . . . . . . . 11 ((t 11c t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ (a t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
133 19.41v 1901 . . . . . . . . . . 11 (a(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ (a t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
134132, 133bitr4i 243 . . . . . . . . . 10 ((t 11c t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ a(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
135134exbii 1582 . . . . . . . . 9 (t(t 11c t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ ta(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
136 df-rex 2620 . . . . . . . . 9 (t 1 1ct, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) ↔ t(t 11c t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
137 excom 1741 . . . . . . . . 9 (at(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))) ↔ ta(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
138135, 136, 1373bitr4i 268 . . . . . . . 8 (t 1 1ct, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) ↔ at(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
139130, 138bitri 240 . . . . . . 7 ({m} (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ at(t = {{a}} t, {m}⟫ ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c))))
140 df-rex 2620 . . . . . . 7 (a m ¬ b m n Nn (a n b n) ↔ a(a m ¬ b m n Nn (a n b n)))
141129, 139, 1403bitr4i 268 . . . . . 6 ({m} (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ a m ¬ b m n Nn (a n b n))
142141notbii 287 . . . . 5 (¬ {m} (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ ¬ a m ¬ b m n Nn (a n b n))
14329elcompl 3225 . . . . 5 ({m} ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ ¬ {m} (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c))
144 dfral2 2626 . . . . 5 (a m b m n Nn (a n b n) ↔ ¬ a m ¬ b m n Nn (a n b n))
145142, 143, 1443bitr4i 268 . . . 4 ({m} ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ a m b m n Nn (a n b n))
1462, 145bitri 240 . . 3 (m 1 ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) ↔ a m b m n Nn (a n b n))
147146abbi2i 2464 . 2 1 ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) = {m a m b m n Nn (a n b n)}
148 ssetkex 4294 . . . . . . 7 Sk V
149148sikex 4297 . . . . . 6 SIk Sk V
150149ins2kex 4307 . . . . . . . 8 Ins2k SIk Sk V
151148ins2kex 4307 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk V
152149ins3kex 4308 . . . . . . . . . . . . . . . . . . . 20 Ins3k SIk Sk V
153151, 152symdifex 4108 . . . . . . . . . . . . . . . . . . 19 ( Ins2k SkIns3k SIk Sk ) V
154 1cex 4142 . . . . . . . . . . . . . . . . . . . . 21 1c V
155154pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 11c V
156155pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 111c V
157153, 156imakex 4300 . . . . . . . . . . . . . . . . . 18 (( Ins2k SkIns3k SIk Sk ) “k 111c) V
158157complex 4104 . . . . . . . . . . . . . . . . 17 ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
159158cnvkex 4287 . . . . . . . . . . . . . . . 16 k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
160159sikex 4297 . . . . . . . . . . . . . . 15 SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
161160ins2kex 4307 . . . . . . . . . . . . . 14 Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
162148ins3kex 4308 . . . . . . . . . . . . . 14 Ins3k Sk V
163161, 162inex 4105 . . . . . . . . . . . . 13 ( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) V
164163, 156imakex 4300 . . . . . . . . . . . 12 (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) V
165164ins2kex 4307 . . . . . . . . . . 11 Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) V
166158sikex 4297 . . . . . . . . . . . . . . . 16 SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
167166cnvkex 4287 . . . . . . . . . . . . . . 15 k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
168167ins2kex 4307 . . . . . . . . . . . . . 14 Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) V
169168, 162inex 4105 . . . . . . . . . . . . 13 ( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) V
170169, 156imakex 4300 . . . . . . . . . . . 12 (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) V
171170ins3kex 4308 . . . . . . . . . . 11 Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) V
172165, 171inex 4105 . . . . . . . . . 10 ( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) V
173 nncex 4396 . . . . . . . . . . . 12 Nn V
174173pw1ex 4303 . . . . . . . . . . 11 1 Nn V
175174pw1ex 4303 . . . . . . . . . 10 11 Nn V
176172, 175imakex 4300 . . . . . . . . 9 (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) V
177176ins3kex 4308 . . . . . . . 8 Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn ) V
178150, 177difex 4107 . . . . . . 7 ( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) V
179156pw1ex 4303 . . . . . . 7 1111c V
180178, 179imakex 4300 . . . . . 6 (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c) V
181149, 180inex 4105 . . . . 5 ( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) V
182181, 155imakex 4300 . . . 4 (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) V
183182complex 4104 . . 3 ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) V
184183uni1ex 4293 . 2 1 ∼ (( SIk Sk ∩ (( Ins2k SIk Sk Ins3k (( Ins2k (( Ins2k SIk k ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c) ∩ Ins3k (( Ins2k k SIk ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11 Nn )) “k 1111c)) “k 11c) V
185147, 184eqeltrri 2424 1 {m a m b m n Nn (a n b n)} V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209  ℘cpw 3722  {csn 3737  ⟪copk 4057  ⋃1cuni1 4133  1cc1c 4134  ℘1cpw1 4135  ◡kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  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-sbc 3047  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-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378  df-nnc 4379 This theorem is referenced by:  nnpweq  4523
 Copyright terms: Public domain W3C validator