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

Theorem nnsucelrlem1 4424
Description: Lemma for nnsucelr 4428. Establish stratification for the inductive hypothesis. (Contributed by SF, 15-Jan-2015.)
Assertion
Ref Expression
nnsucelrlem1 {m ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m)} V
Distinct variable group:   m,a,x

Proof of Theorem nnsucelrlem1
Dummy variables e t w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . . 8 m V
21elimak 4259 . . . . . . 7 (m (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ t 1ct, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c))
3 df-rex 2620 . . . . . . . 8 (t 1ct, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ t(t 1c t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
4 el1c 4139 . . . . . . . . . . . 12 (t 1ca t = {a})
54anbi1i 676 . . . . . . . . . . 11 ((t 1c t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ (a t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
6 19.41v 1901 . . . . . . . . . . 11 (a(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ (a t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
75, 6bitr4i 243 . . . . . . . . . 10 ((t 1c t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ a(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
87exbii 1582 . . . . . . . . 9 (t(t 1c t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ ta(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
9 excom 1741 . . . . . . . . 9 (at(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ ta(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
108, 9bitr4i 243 . . . . . . . 8 (t(t 1c t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ at(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
113, 10bitri 240 . . . . . . 7 (t 1ct, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ at(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
122, 11bitri 240 . . . . . 6 (m (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ at(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
13 snex 4111 . . . . . . . . 9 {a} V
14 opkeq1 4059 . . . . . . . . . 10 (t = {a} → ⟪t, m⟫ = ⟪{a}, m⟫)
1514eleq1d 2419 . . . . . . . . 9 (t = {a} → (⟪t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ ⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)))
1613, 15ceqsexv 2894 . . . . . . . 8 (t(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ ⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c))
17 opkex 4113 . . . . . . . . . . . 12 ⟪{a}, m V
1817elimak 4259 . . . . . . . . . . 11 (⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ t 1 111ct, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )))
19 df-rex 2620 . . . . . . . . . . . 12 (t 1 111ct, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ t(t 1111c t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
20 elpw131c 4149 . . . . . . . . . . . . . . . 16 (t 1111cx t = {{{{x}}}})
2120anbi1i 676 . . . . . . . . . . . . . . 15 ((t 1111c t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ (x t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
22 19.41v 1901 . . . . . . . . . . . . . . 15 (x(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ (x t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
2321, 22bitr4i 243 . . . . . . . . . . . . . 14 ((t 1111c t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ x(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
2423exbii 1582 . . . . . . . . . . . . 13 (t(t 1111c t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ tx(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
25 excom 1741 . . . . . . . . . . . . 13 (xt(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ tx(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
2624, 25bitr4i 243 . . . . . . . . . . . 12 (t(t 1111c t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ xt(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
2719, 26bitri 240 . . . . . . . . . . 11 (t 1 111ct, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ xt(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
2818, 27bitri 240 . . . . . . . . . 10 (⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ xt(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
29 snex 4111 . . . . . . . . . . . . 13 {{{{x}}}} V
30 opkeq1 4059 . . . . . . . . . . . . . 14 (t = {{{{x}}}} → ⟪t, ⟪{a}, m⟫⟫ = ⟪{{{{x}}}}, ⟪{a}, m⟫⟫)
3130eleq1d 2419 . . . . . . . . . . . . 13 (t = {{{{x}}}} → (⟪t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))))
3229, 31ceqsexv 2894 . . . . . . . . . . . 12 (t(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )))
33 eldif 3221 . . . . . . . . . . . . . 14 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk )))
34 eldif 3221 . . . . . . . . . . . . . . . . 17 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk ))
35 opkex 4113 . . . . . . . . . . . . . . . . . . . . 21 ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ V
3635elimak 4259 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) ↔ t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )))
37 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
38 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t 11111cw t = {{{{{w}}}}})
3938anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((t 11111c t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ (w t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
40 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (w(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ (w t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
4139, 40bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 11111c t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ w(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
4241exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ tw(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
43 excom 1741 . . . . . . . . . . . . . . . . . . . . . . 23 (wt(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ tw(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
4442, 43bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22 (t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ wt(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
4537, 44bitri 240 . . . . . . . . . . . . . . . . . . . . 21 (t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ wt(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
46 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {{{{{w}}}}} V
47 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{{{{w}}}}} → ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ = ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫)
4847eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 (t = {{{{{w}}}}} → (⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))))
4946, 48ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )))
50 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )))
51 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ V
5251elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )))
53 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t 1 1111111ct, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ t(t 11111111c t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
54 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t 11111111ce t = {{{{{{{{e}}}}}}}})
5554anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((t 11111111c t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ (e t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
56 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (e(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ (e t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
5755, 56bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((t 11111111c t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ e(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
5857exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t(t 11111111c t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ te(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
59 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (et(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ te(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
6058, 59bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t 11111111c t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ et(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
6153, 60bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t 1 1111111ct, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ et(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
6252, 61bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ et(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
63 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{{{{{{{e}}}}}}}} V
64 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t = {{{{{{{{e}}}}}}}} → ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ = ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫)
6564eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{{{{{{e}}}}}}}} → (⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))))
6663, 65ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )))
67 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ ¬ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins2k ( Ins2k Ins3k SIk SkIns3k Ik )))
68 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {{{{{{e}}}}}} V
6968, 46, 35otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ SIk SIk SIk SIk SIk Sk )
70 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{{{{e}}}}} V
71 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{{{w}}}} V
7270, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{e}}}}}, {{{{w}}}}⟫ SIk SIk SIk SIk Sk )
73 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{{e}}}} V
74 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{w}}} V
7573, 74opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{e}}}}}, {{{{w}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{e}}}}, {{{w}}}⟫ SIk SIk SIk Sk )
76 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{{e}}} V
77 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{w}} V
7876, 77opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{e}}}}, {{{w}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{e}}}, {{w}}⟫ SIk SIk Sk )
79 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{e}} V
80 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {w} V
8179, 80opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{e}}}, {{w}}⟫ SIk SIk Sk ↔ ⟪{{e}}, {w}⟫ SIk Sk )
82 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {e} V
83 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 w V
8482, 83opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{e}}, {w}⟫ SIk Sk ↔ ⟪{e}, w Sk )
85 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 e V
8685, 83elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{e}, w Ske w)
8784, 86bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{e}}, {w}⟫ SIk Ske w)
8881, 87bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{e}}}, {{w}}⟫ SIk SIk Ske w)
8978, 88bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{e}}}}, {{{w}}}⟫ SIk SIk SIk Ske w)
9075, 89bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{e}}}}}, {{{{w}}}}⟫ SIk SIk SIk SIk Ske w)
9172, 90bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ SIk SIk SIk SIk SIk Ske w)
9269, 91bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Ske w)
9368, 46, 35otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins2k ( Ins2k Ins3k SIk SkIns3k Ik ) ↔ ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( Ins2k Ins3k SIk SkIns3k Ik ))
9473, 29, 17otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins3k SIk Sk ↔ ⟪{{{{e}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk )
9579, 13, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{e}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk ↔ ⟪{{e}}, {a}⟫ SIk Sk )
96 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 a V
9782, 96opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{e}}, {a}⟫ SIk Sk ↔ ⟪{e}, a Sk )
9885, 96elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{e}, a Ske a)
9997, 98bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{e}}, {a}⟫ SIk Ske a)
10095, 99bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{e}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Ske a)
10194, 100bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins3k SIk Ske a)
10273, 29, 17otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins3k Ik ↔ ⟪{{{{e}}}}, {{{{x}}}}⟫ Ik )
10376sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ({{{{e}}}} = {{{{x}}}} ↔ {{{e}}} = {{{x}}})
10479sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ({{{e}}} = {{{x}}} ↔ {{e}} = {{x}})
10582sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ({{e}} = {{x}} ↔ {e} = {x})
10685sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ({e} = {x} ↔ e = x)
107105, 106bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ({{e}} = {{x}} ↔ e = x)
108104, 107bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ({{{e}}} = {{{x}}} ↔ e = x)
109103, 108bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({{{{e}}}} = {{{{x}}}} ↔ e = x)
110 opkelidkg 4274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (({{{{e}}}} V {{{{x}}}} V) → (⟪{{{{e}}}}, {{{{x}}}}⟫ Ik ↔ {{{{e}}}} = {{{{x}}}}))
11173, 29, 110mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{e}}}}, {{{{x}}}}⟫ Ik ↔ {{{{e}}}} = {{{{x}}}})
11285elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (e {x} ↔ e = x)
113109, 111, 1123bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{e}}}}, {{{{x}}}}⟫ Ike {x})
114102, 113bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins3k Ike {x})
115101, 114orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins3k SIk Sk ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins3k Ik ) ↔ (e a e {x}))
116 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( Ins2k Ins3k SIk SkIns3k Ik ) ↔ (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins3k SIk Sk ⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins3k Ik ))
117 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (e (a ∪ {x}) ↔ (e a e {x}))
118115, 116, 1173bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( Ins2k Ins3k SIk SkIns3k Ik ) ↔ e (a ∪ {x}))
11993, 118bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins2k ( Ins2k Ins3k SIk SkIns3k Ik ) ↔ e (a ∪ {x}))
12092, 119bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ (e we (a ∪ {x})))
121120notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (¬ (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ Ins2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ ¬ (e we (a ∪ {x})))
12267, 121bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) ↔ ¬ (e we (a ∪ {x})))
12366, 122bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ ¬ (e we (a ∪ {x})))
124123exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (et(t = {{{{{{{{e}}}}}}}} t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik ))) ↔ e ¬ (e we (a ∪ {x})))
12562, 124bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ e ¬ (e we (a ∪ {x})))
126125notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ ¬ e ¬ (e we (a ∪ {x})))
12751elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ ¬ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c))
128 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (w = (a ∪ {x}) ↔ e(e we (a ∪ {x})))
129 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (e(e we (a ∪ {x})) ↔ ¬ e ¬ (e we (a ∪ {x})))
130128, 129bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (w = (a ∪ {x}) ↔ ¬ e ¬ (e we (a ∪ {x})))
131126, 127, 1303bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ↔ w = (a ∪ {x}))
13274, 29, 17otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ ⟪{{{w}}}, ⟪{a}, m⟫⟫ Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))
13380, 13, 1otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{w}}}, ⟪{a}, m⟫⟫ Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ ⟪{w}, m (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))
134 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⟪{w}, t Sk t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ (⟪t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ⟪{w}, t Sk ))
135 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 t V
136135, 1opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ ⟪m, t Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))
137 opkelimagekg 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((m V t V) → (⟪m, t Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ t = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k m)))
1381, 135, 137mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪m, t Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ t = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k m))
139 dfaddc2 4381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (m +c 1c) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k m)
140139eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t = (m +c 1c) ↔ t = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k m))
141140bicomi 193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k m) ↔ t = (m +c 1c))
142138, 141bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪m, t Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ t = (m +c 1c))
143136, 142bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ t = (m +c 1c))
14483, 135elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{w}, t Skw t)
145143, 144anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⟪t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ⟪{w}, t Sk ) ↔ (t = (m +c 1c) w t))
146134, 145bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟪{w}, t Sk t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ (t = (m +c 1c) w t))
147146exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(⟪{w}, t Sk t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ t(t = (m +c 1c) w t))
14880, 1opkelcok 4262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{w}, m (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ t(⟪{w}, t Sk t, m kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
149 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1c V
1501, 149addcex 4394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (m +c 1c) V
151150clel3 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (w (m +c 1c) ↔ t(t = (m +c 1c) w t))
152147, 148, 1513bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{w}, m (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ w (m +c 1c))
153133, 152bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{w}}}, ⟪{a}, m⟫⟫ Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ w (m +c 1c))
154132, 153bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) ↔ w (m +c 1c))
155131, 154anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ (w = (a ∪ {x}) w (m +c 1c)))
15650, 155bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ (w = (a ∪ {x}) w (m +c 1c)))
15749, 156bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (t(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ (w = (a ∪ {x}) w (m +c 1c)))
158157exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (wt(t = {{{{{w}}}}} t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ))) ↔ w(w = (a ∪ {x}) w (m +c 1c)))
15945, 158bitri 240 . . . . . . . . . . . . . . . . . . . 20 (t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) ↔ w(w = (a ∪ {x}) w (m +c 1c)))
16036, 159bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) ↔ w(w = (a ∪ {x}) w (m +c 1c)))
161 df-clel 2349 . . . . . . . . . . . . . . . . . . 19 ((a ∪ {x}) (m +c 1c) ↔ w(w = (a ∪ {x}) w (m +c 1c)))
162160, 161bitr4i 243 . . . . . . . . . . . . . . . . . 18 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) ↔ (a ∪ {x}) (m +c 1c))
163 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{x}} V
164163, 13, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk ↔ ⟪{{x}}, {a}⟫ SIk Sk )
165 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {x} V
166165, 96opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{x}}, {a}⟫ SIk Sk ↔ ⟪{x}, a Sk )
167 vex 2862 . . . . . . . . . . . . . . . . . . . . . 22 x V
168167, 96elssetk 4270 . . . . . . . . . . . . . . . . . . . . 21 (⟪{x}, a Skx a)
169166, 168bitri 240 . . . . . . . . . . . . . . . . . . . 20 (⟪{{x}}, {a}⟫ SIk Skx a)
170164, 169bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Skx a)
171170notbii 287 . . . . . . . . . . . . . . . . . 18 (¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk ↔ ¬ x a)
172162, 171anbi12i 678 . . . . . . . . . . . . . . . . 17 ((⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ Ins3k SIk Sk ) ↔ ((a ∪ {x}) (m +c 1c) ¬ x a))
17334, 172bitri 240 . . . . . . . . . . . . . . . 16 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) ↔ ((a ∪ {x}) (m +c 1c) ¬ x a))
174 ancom 437 . . . . . . . . . . . . . . . 16 (((a ∪ {x}) (m +c 1c) ¬ x a) ↔ (¬ x a (a ∪ {x}) (m +c 1c)))
175173, 174bitri 240 . . . . . . . . . . . . . . 15 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) ↔ (¬ x a (a ∪ {x}) (m +c 1c)))
17629, 17opkelxpk 4248 . . . . . . . . . . . . . . . . . 18 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk ) ↔ ({{{{x}}}} V ⟪{a}, m Sk ))
17729, 176mpbiran 884 . . . . . . . . . . . . . . . . 17 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk ) ↔ ⟪{a}, m Sk )
17896, 1elssetk 4270 . . . . . . . . . . . . . . . . 17 (⟪{a}, m Ska m)
179177, 178bitri 240 . . . . . . . . . . . . . . . 16 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk ) ↔ a m)
180179notbii 287 . . . . . . . . . . . . . . 15 (¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk ) ↔ ¬ a m)
181175, 180anbi12i 678 . . . . . . . . . . . . . 14 ((⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (V ×k Sk )) ↔ ((¬ x a (a ∪ {x}) (m +c 1c)) ¬ a m))
18233, 181bitri 240 . . . . . . . . . . . . 13 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ ((¬ x a (a ∪ {x}) (m +c 1c)) ¬ a m))
183 annim 414 . . . . . . . . . . . . 13 (((¬ x a (a ∪ {x}) (m +c 1c)) ¬ a m) ↔ ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
184182, 183bitri 240 . . . . . . . . . . . 12 (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) ↔ ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
18532, 184bitri 240 . . . . . . . . . . 11 (t(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
186185exbii 1582 . . . . . . . . . 10 (xt(t = {{{{x}}}} t, ⟪{a}, m⟫⟫ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk ))) ↔ x ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
18728, 186bitri 240 . . . . . . . . 9 (⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ x ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
188 exnal 1574 . . . . . . . . 9 (x ¬ ((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
189187, 188bitri 240 . . . . . . . 8 (⟪{a}, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) ↔ ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
19016, 189bitri 240 . . . . . . 7 (t(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
191190exbii 1582 . . . . . 6 (at(t = {a} t, m ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c)) ↔ a ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
19212, 191bitri 240 . . . . 5 (m (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ a ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
193192notbii 287 . . . 4 m (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ ¬ a ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
1941elcompl 3225 . . . 4 (m ∼ (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ ¬ m (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c))
195 alex 1572 . . . 4 (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ¬ a ¬ x((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
196193, 194, 1953bitr4i 268 . . 3 (m ∼ (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) ↔ ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m))
197196abbi2i 2464 . 2 ∼ (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) = {m ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m)}
198 ssetkex 4294 . . . . . . . . . . . . . . . . . 18 Sk V
199198sikex 4297 . . . . . . . . . . . . . . . . 17 SIk Sk V
200199sikex 4297 . . . . . . . . . . . . . . . 16 SIk SIk Sk V
201200sikex 4297 . . . . . . . . . . . . . . 15 SIk SIk SIk Sk V
202201sikex 4297 . . . . . . . . . . . . . 14 SIk SIk SIk SIk Sk V
203202sikex 4297 . . . . . . . . . . . . 13 SIk SIk SIk SIk SIk Sk V
204203ins3kex 4308 . . . . . . . . . . . 12 Ins3k SIk SIk SIk SIk SIk Sk V
205199ins3kex 4308 . . . . . . . . . . . . . . 15 Ins3k SIk Sk V
206205ins2kex 4307 . . . . . . . . . . . . . 14 Ins2k Ins3k SIk Sk V
207 idkex 4314 . . . . . . . . . . . . . . 15 Ik V
208207ins3kex 4308 . . . . . . . . . . . . . 14 Ins3k Ik V
209206, 208unex 4106 . . . . . . . . . . . . 13 ( Ins2k Ins3k SIk SkIns3k Ik ) V
210209ins2kex 4307 . . . . . . . . . . . 12 Ins2k ( Ins2k Ins3k SIk SkIns3k Ik ) V
211204, 210symdifex 4108 . . . . . . . . . . 11 ( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) V
212149pw1ex 4303 . . . . . . . . . . . . . . . . 17 11c V
213212pw1ex 4303 . . . . . . . . . . . . . . . 16 111c V
214213pw1ex 4303 . . . . . . . . . . . . . . 15 1111c V
215214pw1ex 4303 . . . . . . . . . . . . . 14 11111c V
216215pw1ex 4303 . . . . . . . . . . . . 13 111111c V
217216pw1ex 4303 . . . . . . . . . . . 12 1111111c V
218217pw1ex 4303 . . . . . . . . . . 11 11111111c V
219211, 218imakex 4300 . . . . . . . . . 10 (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) V
220219complex 4104 . . . . . . . . 9 ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) V
221 addcexlem 4382 . . . . . . . . . . . . . . 15 ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V
222221, 213imakex 4300 . . . . . . . . . . . . . 14 (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
223222imagekex 4312 . . . . . . . . . . . . 13 Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
224223cnvkex 4287 . . . . . . . . . . . 12 kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
225224, 198cokex 4310 . . . . . . . . . . 11 (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) V
226225ins2kex 4307 . . . . . . . . . 10 Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) V
227226ins2kex 4307 . . . . . . . . 9 Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk ) V
228220, 227inex 4105 . . . . . . . 8 ( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) V
229228, 215imakex 4300 . . . . . . 7 (( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) V
230229, 205difex 4107 . . . . . 6 ((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) V
231 vvex 4109 . . . . . . 7 V V
232231, 198xpkex 4289 . . . . . 6 (V ×k Sk ) V
233230, 232difex 4107 . . . . 5 (((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) V
234233, 214imakex 4300 . . . 4 ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) V
235234, 149imakex 4300 . . 3 (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) V
236235complex 4104 . 2 ∼ (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk SkIns2k ( Ins2k Ins3k SIk SkIns3k Ik )) “k 11111111c) ∩ Ins2k Ins2k (kImagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) k Sk )) “k 11111c) Ins3k SIk Sk ) (V ×k Sk )) “k 1111c) “k 1c) V
237197, 236eqeltrri 2424 1 {m ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m)} V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174  kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   k ccomk 4180   SIk csik 4181  Imagekcimagek 4182   Sk cssetk 4183   Ik cidk 4184   +c cplc 4375
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-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-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-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-idk 4195  df-addc 4378
This theorem is referenced by:  nnsucelr  4428
  Copyright terms: Public domain W3C validator