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

Theorem ncfinlowerlem1 4482
 Description: Lemma for ncfinlower 4483. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)
Assertion
Ref Expression
ncfinlowerlem1 {m ab((1a m 1b m) → n Nn (a n b n))} V
Distinct variable group:   m,n,a,b

Proof of Theorem ncfinlowerlem1
Dummy variables t x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . 7 m V
21elimak 4259 . . . . . 6 (m (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) ↔ t 1 1ct, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c))
3 elpw11c 4147 . . . . . . . . . 10 (t 11ca t = {{a}})
43anbi1i 676 . . . . . . . . 9 ((t 11c t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ (a t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
5 19.41v 1901 . . . . . . . . 9 (a(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ (a t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
64, 5bitr4i 243 . . . . . . . 8 ((t 11c t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ a(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
76exbii 1582 . . . . . . 7 (t(t 11c t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ ta(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
8 df-rex 2620 . . . . . . 7 (t 1 1ct, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) ↔ t(t 11c t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
9 excom 1741 . . . . . . 7 (at(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ ta(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
107, 8, 93bitr4i 268 . . . . . 6 (t 1 1ct, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) ↔ at(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
11 snex 4111 . . . . . . . . 9 {{a}} V
12 opkeq1 4059 . . . . . . . . . 10 (t = {{a}} → ⟪t, m⟫ = ⟪{{a}}, m⟫)
1312eleq1d 2419 . . . . . . . . 9 (t = {{a}} → (⟪t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) ↔ ⟪{{a}}, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)))
1411, 13ceqsexv 2894 . . . . . . . 8 (t(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ ⟪{{a}}, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c))
15 opkex 4113 . . . . . . . . . 10 ⟪{{a}}, m V
1615elimak 4259 . . . . . . . . 9 (⟪{{a}}, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) ↔ t 1 111ct, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )))
17 elpw131c 4149 . . . . . . . . . . . . 13 (t 1111cb t = {{{{b}}}})
1817anbi1i 676 . . . . . . . . . . . 12 ((t 1111c t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ (b t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
19 19.41v 1901 . . . . . . . . . . . 12 (b(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ (b t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
2018, 19bitr4i 243 . . . . . . . . . . 11 ((t 1111c t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ b(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
2120exbii 1582 . . . . . . . . . 10 (t(t 1111c t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ tb(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
22 df-rex 2620 . . . . . . . . . 10 (t 1 111ct, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) ↔ t(t 1111c t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
23 excom 1741 . . . . . . . . . 10 (bt(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ tb(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
2421, 22, 233bitr4i 268 . . . . . . . . 9 (t 1 111ct, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) ↔ bt(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
25 snex 4111 . . . . . . . . . . . 12 {{{{b}}}} V
26 opkeq1 4059 . . . . . . . . . . . . 13 (t = {{{{b}}}} → ⟪t, ⟪{{a}}, m⟫⟫ = ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫)
2726eleq1d 2419 . . . . . . . . . . . 12 (t = {{{{b}}}} → (⟪t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) ↔ ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))))
2825, 27ceqsexv 2894 . . . . . . . . . . 11 (t(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )))
29 eldif 3221 . . . . . . . . . . 11 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) ↔ (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ ((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ¬ ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )))
30 elin 3219 . . . . . . . . . . . . 13 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ ((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)))
3115elimak 4259 . . . . . . . . . . . . . . . 16 (⟪{{a}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
32 elpw121c 4148 . . . . . . . . . . . . . . . . . . . 20 (t 111cx t = {{{x}}})
3332anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 111c t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
34 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (x(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
3533, 34bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 111c t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
3635exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 111c t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
37 df-rex 2620 . . . . . . . . . . . . . . . . 17 (t 1 11ct, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
38 excom 1741 . . . . . . . . . . . . . . . . 17 (xt(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
3936, 37, 383bitr4i 268 . . . . . . . . . . . . . . . 16 (t 1 11ct, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ xt(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
40 snex 4111 . . . . . . . . . . . . . . . . . . 19 {{{x}}} V
41 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20 (t = {{{x}}} → ⟪t, ⟪{{a}}, m⟫⟫ = ⟪{{{x}}}, ⟪{{a}}, m⟫⟫)
4241eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (t = {{{x}}} → (⟪t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ ⟪{{{x}}}, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
4340, 42ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (t(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ⟪{{{x}}}, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
44 elin 3219 . . . . . . . . . . . . . . . . . 18 (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins2k Sk ))
45 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {x} V
4645, 11, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪{x}, {{a}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
47 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 x V
48 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {a} V
4947, 48opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 (⟪{x}, {{a}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪x, {a}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
50 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 a V
5147, 50eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . 20 (⟪x, {a}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1a)
5246, 49, 513bitri 262 . . . . . . . . . . . . . . . . . . 19 (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1a)
5345, 11, 1otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins2k Sk ↔ ⟪{x}, m Sk )
5447, 1elssetk 4270 . . . . . . . . . . . . . . . . . . . 20 (⟪{x}, m Skx m)
5553, 54bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins2k Skx m)
5652, 55anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{a}}, m⟫⟫ Ins2k Sk ) ↔ (x = 1a x m))
5743, 44, 563bitri 262 . . . . . . . . . . . . . . . . 17 (t(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x = 1a x m))
5857exbii 1582 . . . . . . . . . . . . . . . 16 (xt(t = {{{x}}} t, ⟪{{a}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(x = 1a x m))
5931, 39, 583bitri 262 . . . . . . . . . . . . . . 15 (⟪{{a}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ x(x = 1a x m))
6025, 15opkelxpk 4248 . . . . . . . . . . . . . . . 16 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ ({{{{b}}}} V ⟪{{a}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)))
6125, 60mpbiran 884 . . . . . . . . . . . . . . 15 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ ⟪{{a}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))
62 df-clel 2349 . . . . . . . . . . . . . . 15 (1a mx(x = 1a x m))
6359, 61, 623bitr4i 268 . . . . . . . . . . . . . 14 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ 1a m)
64 opkex 4113 . . . . . . . . . . . . . . . . 17 ⟪{{b}}, m V
6564elimak 4259 . . . . . . . . . . . . . . . 16 (⟪{{b}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
6632anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 111c t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
67 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (x(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
6866, 67bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 111c t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
6968exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 111c t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
70 df-rex 2620 . . . . . . . . . . . . . . . . 17 (t 1 11ct, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
71 excom 1741 . . . . . . . . . . . . . . . . 17 (xt(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
7269, 70, 713bitr4i 268 . . . . . . . . . . . . . . . 16 (t 1 11ct, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ xt(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
73 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20 (t = {{{x}}} → ⟪t, ⟪{{b}}, m⟫⟫ = ⟪{{{x}}}, ⟪{{b}}, m⟫⟫)
7473eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (t = {{{x}}} → (⟪t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ ⟪{{{x}}}, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
7540, 74ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (t(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ⟪{{{x}}}, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
76 elin 3219 . . . . . . . . . . . . . . . . . 18 (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins2k Sk ))
77 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{b}} V
7845, 77, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪{x}, {{b}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
79 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {b} V
8047, 79opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 (⟪{x}, {{b}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪x, {b}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
81 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 b V
8247, 81eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . 20 (⟪x, {b}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1b)
8378, 80, 823bitri 262 . . . . . . . . . . . . . . . . . . 19 (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1b)
8445, 77, 1otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins2k Sk ↔ ⟪{x}, m Sk )
8584, 54bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins2k Skx m)
8683, 85anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{b}}, m⟫⟫ Ins2k Sk ) ↔ (x = 1b x m))
8775, 76, 863bitri 262 . . . . . . . . . . . . . . . . 17 (t(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x = 1b x m))
8887exbii 1582 . . . . . . . . . . . . . . . 16 (xt(t = {{{x}}} t, ⟪{{b}}, m⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(x = 1b x m))
8965, 72, 883bitri 262 . . . . . . . . . . . . . . 15 (⟪{{b}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ x(x = 1b x m))
9077, 11, 1otkelins2k 4255 . . . . . . . . . . . . . . 15 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ ⟪{{b}}, m (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))
91 df-clel 2349 . . . . . . . . . . . . . . 15 (1b mx(x = 1b x m))
9289, 90, 913bitr4i 268 . . . . . . . . . . . . . 14 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ 1b m)
9363, 92anbi12i 678 . . . . . . . . . . . . 13 ((⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ (1a m 1b m))
9430, 93bitri 240 . . . . . . . . . . . 12 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ ((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ (1a m 1b m))
9577, 11, 1otkelins3k 4256 . . . . . . . . . . . . . 14 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ ⟪{{b}}, {{a}}⟫ SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))
9679, 48opksnelsik 4265 . . . . . . . . . . . . . 14 (⟪{{b}}, {{a}}⟫ SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ ⟪{b}, {a}⟫ (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))
97 opkex 4113 . . . . . . . . . . . . . . . 16 ⟪{b}, {a}⟫ V
9897elimak 4259 . . . . . . . . . . . . . . 15 (⟪{b}, {a}⟫ (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ t 1 1 Nnt, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ))
99 elpw12 4145 . . . . . . . . . . . . . . . . . . 19 (t 11 Nnn Nn t = {{n}})
10099anbi1i 676 . . . . . . . . . . . . . . . . . 18 ((t 11 Nn t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ (n Nn t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
101 r19.41v 2764 . . . . . . . . . . . . . . . . . 18 (n Nn (t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ (n Nn t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
102100, 101bitr4i 243 . . . . . . . . . . . . . . . . 17 ((t 11 Nn t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ n Nn (t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
103102exbii 1582 . . . . . . . . . . . . . . . 16 (t(t 11 Nn t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ tn Nn (t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
104 df-rex 2620 . . . . . . . . . . . . . . . 16 (t 1 1 Nnt, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ) ↔ t(t 11 Nn t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
105 rexcom4 2878 . . . . . . . . . . . . . . . 16 (n Nn t(t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ tn Nn (t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
106103, 104, 1053bitr4i 268 . . . . . . . . . . . . . . 15 (t 1 1 Nnt, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ) ↔ n Nn t(t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
107 snex 4111 . . . . . . . . . . . . . . . . . 18 {{n}} V
108 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19 (t = {{n}} → ⟪t, ⟪{b}, {a}⟫⟫ = ⟪{{n}}, ⟪{b}, {a}⟫⟫)
109108eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (t = {{n}} → (⟪t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ) ↔ ⟪{{n}}, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )))
110107, 109ceqsexv 2894 . . . . . . . . . . . . . . . . 17 (t(t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ ⟪{{n}}, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ))
111 elin 3219 . . . . . . . . . . . . . . . . 17 (⟪{{n}}, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk ) ↔ (⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins2k k Sk ⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins3k k Sk ))
112 vex 2862 . . . . . . . . . . . . . . . . . . . 20 n V
113112, 79, 48otkelins2k 4255 . . . . . . . . . . . . . . . . . . 19 (⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins2k k Sk ↔ ⟪n, {a}⟫ k Sk )
114112, 48opkelcnvk 4250 . . . . . . . . . . . . . . . . . . 19 (⟪n, {a}⟫ k Sk ↔ ⟪{a}, n Sk )
11550, 112elssetk 4270 . . . . . . . . . . . . . . . . . . 19 (⟪{a}, n Ska n)
116113, 114, 1153bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins2k k Ska n)
117112, 79, 48otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 (⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins3k k Sk ↔ ⟪n, {b}⟫ k Sk )
118112, 79opkelcnvk 4250 . . . . . . . . . . . . . . . . . . 19 (⟪n, {b}⟫ k Sk ↔ ⟪{b}, n Sk )
11981, 112elssetk 4270 . . . . . . . . . . . . . . . . . . 19 (⟪{b}, n Skb n)
120117, 118, 1193bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins3k k Skb n)
121116, 120anbi12i 678 . . . . . . . . . . . . . . . . 17 ((⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins2k k Sk ⟪{{n}}, ⟪{b}, {a}⟫⟫ Ins3k k Sk ) ↔ (a n b n))
122110, 111, 1213bitri 262 . . . . . . . . . . . . . . . 16 (t(t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ (a n b n))
123122rexbii 2639 . . . . . . . . . . . . . . 15 (n Nn t(t = {{n}} t, ⟪{b}, {a}⟫⟫ ( Ins2k k SkIns3k k Sk )) ↔ n Nn (a n b n))
12498, 106, 1233bitri 262 . . . . . . . . . . . . . 14 (⟪{b}, {a}⟫ (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ n Nn (a n b n))
12595, 96, 1243bitri 262 . . . . . . . . . . . . 13 (⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ n Nn (a n b n))
126125notbii 287 . . . . . . . . . . . 12 (¬ ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) ↔ ¬ n Nn (a n b n))
12794, 126anbi12i 678 . . . . . . . . . . 11 ((⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ ((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ¬ ⟪{{{{b}}}}, ⟪{{a}}, m⟫⟫ Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) ↔ ((1a m 1b m) ¬ n Nn (a n b n)))
12828, 29, 1273bitri 262 . . . . . . . . . 10 (t(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ ((1a m 1b m) ¬ n Nn (a n b n)))
129128exbii 1582 . . . . . . . . 9 (bt(t = {{{{b}}}} t, ⟪{{a}}, m⟫⟫ (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ))) ↔ b((1a m 1b m) ¬ n Nn (a n b n)))
13016, 24, 1293bitri 262 . . . . . . . 8 (⟪{{a}}, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) ↔ b((1a m 1b m) ¬ n Nn (a n b n)))
131 exanali 1585 . . . . . . . 8 (b((1a m 1b m) ¬ n Nn (a n b n)) ↔ ¬ b((1a m 1b m) → n Nn (a n b n)))
13214, 130, 1313bitri 262 . . . . . . 7 (t(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ ¬ b((1a m 1b m) → n Nn (a n b n)))
133132exbii 1582 . . . . . 6 (at(t = {{a}} t, m ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c)) ↔ a ¬ b((1a m 1b m) → n Nn (a n b n)))
1342, 10, 1333bitri 262 . . . . 5 (m (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) ↔ a ¬ b((1a m 1b m) → n Nn (a n b n)))
135134notbii 287 . . . 4 m (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) ↔ ¬ a ¬ b((1a m 1b m) → n Nn (a n b n)))
1361elcompl 3225 . . . 4 (m ∼ (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) ↔ ¬ m (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c))
137 alex 1572 . . . 4 (ab((1a m 1b m) → n Nn (a n b n)) ↔ ¬ a ¬ b((1a m 1b m) → n Nn (a n b n)))
138135, 136, 1373bitr4i 268 . . 3 (m ∼ (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) ↔ ab((1a m 1b m) → n Nn (a n b n)))
139138abbi2i 2464 . 2 ∼ (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) = {m ab((1a m 1b m) → n Nn (a n b n))}
140 vvex 4109 . . . . . . . 8 V V
141 1cex 4142 . . . . . . . . . . . . . . 15 1c V
142141pwex 4329 . . . . . . . . . . . . . 14 1c V
143142, 140xpkex 4289 . . . . . . . . . . . . 13 (1c ×k V) V
144 ssetkex 4294 . . . . . . . . . . . . . . . 16 Sk V
145144ins3kex 4308 . . . . . . . . . . . . . . 15 Ins3k Sk V
146144sikex 4297 . . . . . . . . . . . . . . . 16 SIk Sk V
147146ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k SIk Sk V
148145, 147symdifex 4108 . . . . . . . . . . . . . 14 ( Ins3k SkIns2k SIk Sk ) V
149141pw1ex 4303 . . . . . . . . . . . . . . . 16 11c V
150149pw1ex 4303 . . . . . . . . . . . . . . 15 111c V
151150pw1ex 4303 . . . . . . . . . . . . . 14 1111c V
152148, 151imakex 4300 . . . . . . . . . . . . 13 (( Ins3k SkIns2k SIk Sk ) “k 1111c) V
153143, 152difex 4107 . . . . . . . . . . . 12 ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) V
154153sikex 4297 . . . . . . . . . . 11 SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) V
155154ins3kex 4308 . . . . . . . . . 10 Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) V
156144ins2kex 4307 . . . . . . . . . 10 Ins2k Sk V
157155, 156inex 4105 . . . . . . . . 9 ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) V
158157, 150imakex 4300 . . . . . . . 8 (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) V
159140, 158xpkex 4289 . . . . . . 7 (V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) V
160158ins2kex 4307 . . . . . . 7 Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) V
161159, 160inex 4105 . . . . . 6 ((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) V
162144cnvkex 4287 . . . . . . . . . . 11 k Sk V
163162ins2kex 4307 . . . . . . . . . 10 Ins2k k Sk V
164162ins3kex 4308 . . . . . . . . . 10 Ins3k k Sk V
165163, 164inex 4105 . . . . . . . . 9 ( Ins2k k SkIns3k k Sk ) V
166 nncex 4396 . . . . . . . . . . 11 Nn V
167166pw1ex 4303 . . . . . . . . . 10 1 Nn V
168167pw1ex 4303 . . . . . . . . 9 11 Nn V
169165, 168imakex 4300 . . . . . . . 8 (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) V
170169sikex 4297 . . . . . . 7 SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) V
171170ins3kex 4308 . . . . . 6 Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn ) V
172161, 171difex 4107 . . . . 5 (((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) V
173172, 151imakex 4300 . . . 4 ((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) V
174173, 149imakex 4300 . . 3 (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) V
175174complex 4104 . 2 ∼ (((((V ×k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ∩ Ins2k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) Ins3k SIk (( Ins2k k SkIns3k k Sk ) “k 11 Nn )) “k 1111c) “k 11c) V
176139, 175eqeltrri 2424 1 {m ab((1a m 1b m) → n Nn (a n b n))} V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209  ℘cpw 3722  {csn 3737  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174  ◡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:  ncfinlower  4483
 Copyright terms: Public domain W3C validator