Metamath Proof Explorer

Theorem br6

Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013) (Revised by Mario Carneiro, 3-May-2015)

Ref Expression
Hypotheses br6.1 ⊢a=A→φ↔ψ
br6.2 ⊢b=B→ψ↔χ
br6.3 ⊢c=C→χ↔θ
br6.4 ⊢d=D→θ↔τ
br6.5 ⊢e=E→τ↔η
br6.6 ⊢f=F→η↔ζ
br6.7 ⊢x=X→P=Q
br6.8 ⊢R=pq|∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pp=abc∧q=def∧φ
Assertion br6 ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q→ABCRDEF↔ζ

Proof

Step Hyp Ref Expression
1 br6.1 ⊢a=A→φ↔ψ
2 br6.2 ⊢b=B→ψ↔χ
3 br6.3 ⊢c=C→χ↔θ
4 br6.4 ⊢d=D→θ↔τ
5 br6.5 ⊢e=E→τ↔η
6 br6.6 ⊢f=F→η↔ζ
7 br6.7 ⊢x=X→P=Q
8 br6.8 ⊢R=pq|∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pp=abc∧q=def∧φ
9 opex ⊢ABC∈V
10 opex ⊢DEF∈V
11 eqeq1 ⊢p=ABC→p=abc↔ABC=abc
12 eqcom ⊢ABC=abc↔abc=ABC
13 11 12 bitrdi ⊢p=ABC→p=abc↔abc=ABC
14 13 3anbi1d ⊢p=ABC→p=abc∧q=def∧φ↔abc=ABC∧q=def∧φ
15 14 rexbidv ⊢p=ABC→∃f∈Pp=abc∧q=def∧φ↔∃f∈Pabc=ABC∧q=def∧φ
16 15 2rexbidv ⊢p=ABC→∃d∈P∃e∈P∃f∈Pp=abc∧q=def∧φ↔∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ
17 16 2rexbidv ⊢p=ABC→∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pp=abc∧q=def∧φ↔∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ
18 17 2rexbidv ⊢p=ABC→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pp=abc∧q=def∧φ↔∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ
19 eqeq1 ⊢q=DEF→q=def↔DEF=def
20 eqcom ⊢DEF=def↔def=DEF
21 19 20 bitrdi ⊢q=DEF→q=def↔def=DEF
22 21 3anbi2d ⊢q=DEF→abc=ABC∧q=def∧φ↔abc=ABC∧def=DEF∧φ
23 22 rexbidv ⊢q=DEF→∃f∈Pabc=ABC∧q=def∧φ↔∃f∈Pabc=ABC∧def=DEF∧φ
24 23 2rexbidv ⊢q=DEF→∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ↔∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
25 24 2rexbidv ⊢q=DEF→∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ↔∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
26 25 2rexbidv ⊢q=DEF→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧q=def∧φ↔∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
27 9 10 18 26 8 brab ⊢ABCRDEF↔∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
28 vex ⊢a∈V
29 opex ⊢bc∈V
30 28 29 opth ⊢abc=ABC↔a=A∧bc=BC
31 vex ⊢b∈V
32 vex ⊢c∈V
33 31 32 opth ⊢bc=BC↔b=B∧c=C
34 2 3 sylan9bb ⊢b=B∧c=C→ψ↔θ
35 33 34 sylbi ⊢bc=BC→ψ↔θ
36 1 35 sylan9bb ⊢a=A∧bc=BC→φ↔θ
37 30 36 sylbi ⊢abc=ABC→φ↔θ
38 vex ⊢d∈V
39 opex ⊢ef∈V
40 38 39 opth ⊢def=DEF↔d=D∧ef=EF
41 vex ⊢e∈V
42 vex ⊢f∈V
43 41 42 opth ⊢ef=EF↔e=E∧f=F
44 5 6 sylan9bb ⊢e=E∧f=F→τ↔ζ
45 43 44 sylbi ⊢ef=EF→τ↔ζ
46 4 45 sylan9bb ⊢d=D∧ef=EF→θ↔ζ
47 40 46 sylbi ⊢def=DEF→θ↔ζ
48 37 47 sylan9bb ⊢abc=ABC∧def=DEF→φ↔ζ
49 48 biimp3a ⊢abc=ABC∧def=DEF∧φ→ζ
50 49 a1i ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧x∈S∧a∈P∧b∈P∧c∈P∧d∈P∧e∈P∧f∈P→abc=ABC∧def=DEF∧φ→ζ
51 50 rexlimdva ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧x∈S∧a∈P∧b∈P∧c∈P∧d∈P∧e∈P→∃f∈Pabc=ABC∧def=DEF∧φ→ζ
52 51 rexlimdvva ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧x∈S∧a∈P∧b∈P∧c∈P→∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ→ζ
53 52 rexlimdvva ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧x∈S∧a∈P→∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ→ζ
54 53 rexlimdvva ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ→ζ
55 simpl1 ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧ζ→X∈S
56 simpl2 ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧ζ→A∈Q∧B∈Q∧C∈Q
57 opeq1 ⊢d=D→def=Def
58 57 eqeq1d ⊢d=D→def=DEF↔Def=DEF
59 58 4 3anbi23d ⊢d=D→ABC=ABC∧def=DEF∧θ↔ABC=ABC∧Def=DEF∧τ
60 opeq1 ⊢e=E→ef=Ef
61 60 opeq2d ⊢e=E→Def=DEf
62 61 eqeq1d ⊢e=E→Def=DEF↔DEf=DEF
63 62 5 3anbi23d ⊢e=E→ABC=ABC∧Def=DEF∧τ↔ABC=ABC∧DEf=DEF∧η
64 opeq2 ⊢f=F→Ef=EF
65 64 opeq2d ⊢f=F→DEf=DEF
66 65 eqeq1d ⊢f=F→DEf=DEF↔DEF=DEF
67 66 6 3anbi23d ⊢f=F→ABC=ABC∧DEf=DEF∧η↔ABC=ABC∧DEF=DEF∧ζ
68 eqid ⊢ABC=ABC
69 eqid ⊢DEF=DEF
70 68 69 pm3.2i ⊢ABC=ABC∧DEF=DEF
71 df-3an ⊢ABC=ABC∧DEF=DEF∧ζ↔ABC=ABC∧DEF=DEF∧ζ
72 70 71 mpbiran ⊢ABC=ABC∧DEF=DEF∧ζ↔ζ
73 67 72 bitrdi ⊢f=F→ABC=ABC∧DEf=DEF∧η↔ζ
74 59 63 73 rspc3ev ⊢D∈Q∧E∈Q∧F∈Q∧ζ→∃d∈Q∃e∈Q∃f∈QABC=ABC∧def=DEF∧θ
75 74 3ad2antl3 ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧ζ→∃d∈Q∃e∈Q∃f∈QABC=ABC∧def=DEF∧θ
76 opeq1 ⊢a=A→abc=Abc
77 76 eqeq1d ⊢a=A→abc=ABC↔Abc=ABC
78 77 1 3anbi13d ⊢a=A→abc=ABC∧def=DEF∧φ↔Abc=ABC∧def=DEF∧ψ
79 78 rexbidv ⊢a=A→∃f∈Qabc=ABC∧def=DEF∧φ↔∃f∈QAbc=ABC∧def=DEF∧ψ
80 79 2rexbidv ⊢a=A→∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ↔∃d∈Q∃e∈Q∃f∈QAbc=ABC∧def=DEF∧ψ
81 opeq1 ⊢b=B→bc=Bc
82 81 opeq2d ⊢b=B→Abc=ABc
83 82 eqeq1d ⊢b=B→Abc=ABC↔ABc=ABC
84 83 2 3anbi13d ⊢b=B→Abc=ABC∧def=DEF∧ψ↔ABc=ABC∧def=DEF∧χ
85 84 rexbidv ⊢b=B→∃f∈QAbc=ABC∧def=DEF∧ψ↔∃f∈QABc=ABC∧def=DEF∧χ
86 85 2rexbidv ⊢b=B→∃d∈Q∃e∈Q∃f∈QAbc=ABC∧def=DEF∧ψ↔∃d∈Q∃e∈Q∃f∈QABc=ABC∧def=DEF∧χ
87 opeq2 ⊢c=C→Bc=BC
88 87 opeq2d ⊢c=C→ABc=ABC
89 88 eqeq1d ⊢c=C→ABc=ABC↔ABC=ABC
90 89 3 3anbi13d ⊢c=C→ABc=ABC∧def=DEF∧χ↔ABC=ABC∧def=DEF∧θ
91 90 rexbidv ⊢c=C→∃f∈QABc=ABC∧def=DEF∧χ↔∃f∈QABC=ABC∧def=DEF∧θ
92 91 2rexbidv ⊢c=C→∃d∈Q∃e∈Q∃f∈QABc=ABC∧def=DEF∧χ↔∃d∈Q∃e∈Q∃f∈QABC=ABC∧def=DEF∧θ
93 80 86 92 rspc3ev ⊢A∈Q∧B∈Q∧C∈Q∧∃d∈Q∃e∈Q∃f∈QABC=ABC∧def=DEF∧θ→∃a∈Q∃b∈Q∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
94 56 75 93 syl2anc ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧ζ→∃a∈Q∃b∈Q∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
95 7 rexeqdv ⊢x=X→∃f∈Pabc=ABC∧def=DEF∧φ↔∃f∈Qabc=ABC∧def=DEF∧φ
96 7 95 rexeqbidv ⊢x=X→∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
97 7 96 rexeqbidv ⊢x=X→∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
98 7 97 rexeqbidv ⊢x=X→∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
99 7 98 rexeqbidv ⊢x=X→∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔∃b∈Q∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
100 7 99 rexeqbidv ⊢x=X→∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔∃a∈Q∃b∈Q∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ
101 100 rspcev ⊢X∈S∧∃a∈Q∃b∈Q∃c∈Q∃d∈Q∃e∈Q∃f∈Qabc=ABC∧def=DEF∧φ→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
102 55 94 101 syl2anc ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q∧ζ→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
103 102 ex ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q→ζ→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ
104 54 103 impbid ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q→∃x∈S∃a∈P∃b∈P∃c∈P∃d∈P∃e∈P∃f∈Pabc=ABC∧def=DEF∧φ↔ζ
105 27 104 bitrid ⊢X∈S∧A∈Q∧B∈Q∧C∈Q∧D∈Q∧E∈Q∧F∈Q→ABCRDEF↔ζ