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

Theorem setconslem7 4738
Description: Lemma for the set construction theorems. Reorganized version of setconslem3 4734. (Contributed by SF, 4-Feb-2015.)
Hypotheses
Ref Expression
setconslem7.1 A V
setconslem7.2 B V
setconslem7.3 C V
Assertion
Ref Expression
setconslem7 (⟪{{C}}, ⟪A, B⟫⟫ ∼ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ A = B, C)

Proof of Theorem setconslem7
Dummy variables t x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opkex 4114 . . . . . . 7 ⟪{{C}}, ⟪A, B⟫⟫ V
21elimak 4260 . . . . . 6 (⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ t 1 1111ct, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))))
3 df-rex 2621 . . . . . . 7 (t 1 1111ct, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ t(t 11111c t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
4 elpw141c 4151 . . . . . . . . . . 11 (t 11111cx t = {{{{{x}}}}})
54anbi1i 676 . . . . . . . . . 10 ((t 11111c t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ (x t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
6 19.41v 1901 . . . . . . . . . 10 (x(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ (x t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
75, 6bitr4i 243 . . . . . . . . 9 ((t 11111c t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ x(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
87exbii 1582 . . . . . . . 8 (t(t 11111c t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ tx(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
9 excom 1741 . . . . . . . 8 (xt(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ tx(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
108, 9bitr4i 243 . . . . . . 7 (t(t 11111c t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ xt(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
113, 10bitri 240 . . . . . 6 (t 1 1111ct, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ xt(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
122, 11bitri 240 . . . . 5 (⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ xt(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
13 snex 4112 . . . . . . . 8 {{{{{x}}}}} V
14 opkeq1 4060 . . . . . . . . 9 (t = {{{{{x}}}}} → ⟪t, ⟪{{C}}, ⟪A, B⟫⟫⟫ = ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫)
1514eleq1d 2419 . . . . . . . 8 (t = {{{{{x}}}}} → (⟪t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))))
1613, 15ceqsexv 2895 . . . . . . 7 (t(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))))
17 elsymdif 3224 . . . . . . . 8 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ ¬ (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))))
18 snex 4112 . . . . . . . . . . . 12 {{{x}}} V
19 snex 4112 . . . . . . . . . . . 12 {{C}} V
20 opkex 4114 . . . . . . . . . . . 12 A, B V
2118, 19, 20otkelins2k 4256 . . . . . . . . . . 11 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{x}}}, ⟪A, B⟫⟫ Ins3k Sk )
22 snex 4112 . . . . . . . . . . . . 13 {x} V
23 setconslem7.1 . . . . . . . . . . . . 13 A V
24 setconslem7.2 . . . . . . . . . . . . 13 B V
2522, 23, 24otkelins3k 4257 . . . . . . . . . . . 12 (⟪{{{x}}}, ⟪A, B⟫⟫ Ins3k Sk ↔ ⟪{x}, A Sk )
26 vex 2863 . . . . . . . . . . . . 13 x V
2726, 23elssetk 4271 . . . . . . . . . . . 12 (⟪{x}, A Skx A)
2825, 27bitri 240 . . . . . . . . . . 11 (⟪{{{x}}}, ⟪A, B⟫⟫ Ins3k Skx A)
2921, 28bitri 240 . . . . . . . . . 10 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins3k Skx A)
30 elun 3221 . . . . . . . . . . 11 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)) ↔ (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))
3118, 19, 20otkelins2k 4256 . . . . . . . . . . . . 13 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ ⟪{{{x}}}, ⟪A, B⟫⟫ Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))))
3222, 23, 24otkelins2k 4256 . . . . . . . . . . . . . 14 (⟪{{{x}}}, ⟪A, B⟫⟫ Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ ⟪{x}, B ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))))
3326, 24setconslem1 4732 . . . . . . . . . . . . . 14 (⟪{x}, B ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ y B x = Phi y)
3432, 33bitri 240 . . . . . . . . . . . . 13 (⟪{{{x}}}, ⟪A, B⟫⟫ Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ y B x = Phi y)
3531, 34bitri 240 . . . . . . . . . . . 12 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ y B x = Phi y)
3618, 19, 20otkelins3k 4257 . . . . . . . . . . . . 13 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ ⟪{{{x}}}, {{C}}⟫ SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))
37 snex 4112 . . . . . . . . . . . . . . 15 {{x}} V
38 snex 4112 . . . . . . . . . . . . . . 15 {C} V
3937, 38opksnelsik 4266 . . . . . . . . . . . . . 14 (⟪{{{x}}}, {{C}}⟫ SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ ⟪{{x}}, {C}⟫ SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))
40 setconslem7.3 . . . . . . . . . . . . . . . 16 C V
4122, 40opksnelsik 4266 . . . . . . . . . . . . . . 15 (⟪{{x}}, {C}⟫ SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ ⟪{x}, C (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))
4226, 40setconslem2 4733 . . . . . . . . . . . . . . 15 (⟪{x}, C (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ y C x = ( Phi y ∪ {0c}))
4341, 42bitri 240 . . . . . . . . . . . . . 14 (⟪{{x}}, {C}⟫ SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ y C x = ( Phi y ∪ {0c}))
4439, 43bitri 240 . . . . . . . . . . . . 13 (⟪{{{x}}}, {{C}}⟫ SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ y C x = ( Phi y ∪ {0c}))
4536, 44bitri 240 . . . . . . . . . . . 12 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ y C x = ( Phi y ∪ {0c}))
4635, 45orbi12i 507 . . . . . . . . . . 11 ((⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)) ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c})))
4730, 46bitri 240 . . . . . . . . . 10 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)) ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c})))
4829, 47bibi12i 306 . . . . . . . . 9 ((⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
4948notbii 287 . . . . . . . 8 (¬ (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5017, 49bitri 240 . . . . . . 7 (⟪{{{{{x}}}}}, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) ↔ ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5116, 50bitri 240 . . . . . 6 (t(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5251exbii 1582 . . . . 5 (xt(t = {{{{{x}}}}} t, ⟪{{C}}, ⟪A, B⟫⟫⟫ ( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)))) ↔ x ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5312, 52bitri 240 . . . 4 (⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ x ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
54 exnal 1574 . . . 4 (x ¬ (x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))) ↔ ¬ x(x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5553, 54bitri 240 . . 3 (⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ ¬ x(x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
5655con2bii 322 . 2 (x(x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))) ↔ ¬ ⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c))
57 eqop 4612 . 2 (A = B, Cx(x A ↔ (y B x = Phi y y C x = ( Phi y ∪ {0c}))))
581elcompl 3226 . 2 (⟪{{C}}, ⟪A, B⟫⟫ ∼ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ ¬ ⟪{{C}}, ⟪A, B⟫⟫ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c))
5956, 57, 583bitr4ri 269 1 (⟪{{C}}, ⟪A, B⟫⟫ ∼ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ A = B, C)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wo 357   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  wrex 2616  Vcvv 2860  ccompl 3206   cdif 3207  cun 3208  cin 3209  csymdif 3210  {csn 3738  copk 4058  1cc1c 4135  1cpw1 4136   ×k cxpk 4175  kccnvk 4176   Ins2k cins2k 4177   Ins3k cins3k 4178  k cimak 4180   k ccomk 4181   SIk csik 4182  Imagekcimagek 4183   Sk cssetk 4184   Ik cidk 4185   Nn cnnc 4374  0cc0c 4375  cop 4562   Phi cphi 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-addc 4379  df-nnc 4380  df-phi 4566  df-op 4567
This theorem is referenced by:  df1st2  4739
  Copyright terms: Public domain W3C validator