Metamath Proof Explorer

Theorem genpass

Description: Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
genpass.4 ⊢ dom ⁡ F = 𝑷 × 𝑷
genpass.5 ⊢ f ∈ 𝑷 ∧ g ∈ 𝑷 → f F g ∈ 𝑷
genpass.6 ⊢ f G g G h = f G g G h
Assertion genpass ⊢ A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
2 genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
3 genpass.4 ⊢ dom ⁡ F = 𝑷 × 𝑷
4 genpass.5 ⊢ f ∈ 𝑷 ∧ g ∈ 𝑷 → f F g ∈ 𝑷
5 genpass.6 ⊢ f G g G h = f G g G h
6 1 2 genpelv ⊢ B ∈ 𝑷 ∧ C ∈ 𝑷 → t ∈ B F C ↔ ∃ g ∈ B ∃ h ∈ C t = g G h
7 6 3adant1 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → t ∈ B F C ↔ ∃ g ∈ B ∃ h ∈ C t = g G h
8 7 anbi1d ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → t ∈ B F C ∧ x = f G t ↔ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
9 8 exbidv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ t t ∈ B F C ∧ x = f G t ↔ ∃ t ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
10 df-rex ⊢ ∃ t ∈ B F C x = f G t ↔ ∃ t t ∈ B F C ∧ x = f G t
11 ovex ⊢ g G h ∈ V
12 11 isseti ⊢ ∃ t t = g G h
13 12 biantrur ⊢ x = f G g G h ↔ ∃ t t = g G h ∧ x = f G g G h
14 19.41v ⊢ ∃ t t = g G h ∧ x = f G g G h ↔ ∃ t t = g G h ∧ x = f G g G h
15 13 14 bitr4i ⊢ x = f G g G h ↔ ∃ t t = g G h ∧ x = f G g G h
16 15 rexbii ⊢ ∃ h ∈ C x = f G g G h ↔ ∃ h ∈ C ∃ t t = g G h ∧ x = f G g G h
17 rexcom4 ⊢ ∃ h ∈ C ∃ t t = g G h ∧ x = f G g G h ↔ ∃ t ∃ h ∈ C t = g G h ∧ x = f G g G h
18 16 17 bitri ⊢ ∃ h ∈ C x = f G g G h ↔ ∃ t ∃ h ∈ C t = g G h ∧ x = f G g G h
19 18 rexbii ⊢ ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ g ∈ B ∃ t ∃ h ∈ C t = g G h ∧ x = f G g G h
20 rexcom4 ⊢ ∃ g ∈ B ∃ t ∃ h ∈ C t = g G h ∧ x = f G g G h ↔ ∃ t ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G g G h
21 oveq2 ⊢ t = g G h → f G t = f G g G h
22 21 5 eqtr4di ⊢ t = g G h → f G t = f G g G h
23 22 eqeq2d ⊢ t = g G h → x = f G t ↔ x = f G g G h
24 23 pm5.32i ⊢ t = g G h ∧ x = f G t ↔ t = g G h ∧ x = f G g G h
25 24 rexbii ⊢ ∃ h ∈ C t = g G h ∧ x = f G t ↔ ∃ h ∈ C t = g G h ∧ x = f G g G h
26 r19.41v ⊢ ∃ h ∈ C t = g G h ∧ x = f G t ↔ ∃ h ∈ C t = g G h ∧ x = f G t
27 25 26 bitr3i ⊢ ∃ h ∈ C t = g G h ∧ x = f G g G h ↔ ∃ h ∈ C t = g G h ∧ x = f G t
28 27 rexbii ⊢ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G g G h ↔ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
29 r19.41v ⊢ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t ↔ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
30 28 29 bitri ⊢ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G g G h ↔ ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
31 30 exbii ⊢ ∃ t ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G g G h ↔ ∃ t ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
32 19 20 31 3bitri ⊢ ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ t ∃ g ∈ B ∃ h ∈ C t = g G h ∧ x = f G t
33 9 10 32 3bitr4g ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ t ∈ B F C x = f G t ↔ ∃ g ∈ B ∃ h ∈ C x = f G g G h
34 33 rexbidv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ f ∈ A ∃ t ∈ B F C x = f G t ↔ ∃ f ∈ A ∃ g ∈ B ∃ h ∈ C x = f G g G h
35 4 caovcl ⊢ B ∈ 𝑷 ∧ C ∈ 𝑷 → B F C ∈ 𝑷
36 1 2 genpelv ⊢ A ∈ 𝑷 ∧ B F C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ f ∈ A ∃ t ∈ B F C x = f G t
37 35 36 sylan2 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ f ∈ A ∃ t ∈ B F C x = f G t
38 37 3impb ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ f ∈ A ∃ t ∈ B F C x = f G t
39 4 caovcl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A F B ∈ 𝑷
40 1 2 genpelv ⊢ A F B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ t ∈ A F B ∃ h ∈ C x = t G h
41 39 40 stoic3 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ t ∈ A F B ∃ h ∈ C x = t G h
42 1 2 genpelv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → t ∈ A F B ↔ ∃ f ∈ A ∃ g ∈ B t = f G g
43 42 3adant3 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → t ∈ A F B ↔ ∃ f ∈ A ∃ g ∈ B t = f G g
44 43 anbi1d ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → t ∈ A F B ∧ ∃ h ∈ C x = t G h ↔ ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
45 44 exbidv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ t t ∈ A F B ∧ ∃ h ∈ C x = t G h ↔ ∃ t ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
46 df-rex ⊢ ∃ t ∈ A F B ∃ h ∈ C x = t G h ↔ ∃ t t ∈ A F B ∧ ∃ h ∈ C x = t G h
47 19.41v ⊢ ∃ t t = f G g ∧ ∃ h ∈ C x = f G g G h ↔ ∃ t t = f G g ∧ ∃ h ∈ C x = f G g G h
48 oveq1 ⊢ t = f G g → t G h = f G g G h
49 48 eqeq2d ⊢ t = f G g → x = t G h ↔ x = f G g G h
50 49 rexbidv ⊢ t = f G g → ∃ h ∈ C x = t G h ↔ ∃ h ∈ C x = f G g G h
51 50 pm5.32i ⊢ t = f G g ∧ ∃ h ∈ C x = t G h ↔ t = f G g ∧ ∃ h ∈ C x = f G g G h
52 51 exbii ⊢ ∃ t t = f G g ∧ ∃ h ∈ C x = t G h ↔ ∃ t t = f G g ∧ ∃ h ∈ C x = f G g G h
53 ovex ⊢ f G g ∈ V
54 53 isseti ⊢ ∃ t t = f G g
55 54 biantrur ⊢ ∃ h ∈ C x = f G g G h ↔ ∃ t t = f G g ∧ ∃ h ∈ C x = f G g G h
56 47 52 55 3bitr4ri ⊢ ∃ h ∈ C x = f G g G h ↔ ∃ t t = f G g ∧ ∃ h ∈ C x = t G h
57 56 rexbii ⊢ ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ g ∈ B ∃ t t = f G g ∧ ∃ h ∈ C x = t G h
58 rexcom4 ⊢ ∃ g ∈ B ∃ t t = f G g ∧ ∃ h ∈ C x = t G h ↔ ∃ t ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
59 57 58 bitri ⊢ ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ t ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
60 59 rexbii ⊢ ∃ f ∈ A ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ f ∈ A ∃ t ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
61 rexcom4 ⊢ ∃ f ∈ A ∃ t ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h ↔ ∃ t ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
62 r19.41vv ⊢ ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h ↔ ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
63 62 exbii ⊢ ∃ t ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h ↔ ∃ t ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
64 60 61 63 3bitri ⊢ ∃ f ∈ A ∃ g ∈ B ∃ h ∈ C x = f G g G h ↔ ∃ t ∃ f ∈ A ∃ g ∈ B t = f G g ∧ ∃ h ∈ C x = t G h
65 45 46 64 3bitr4g ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ t ∈ A F B ∃ h ∈ C x = t G h ↔ ∃ f ∈ A ∃ g ∈ B ∃ h ∈ C x = f G g G h
66 41 65 bitrd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ ∃ f ∈ A ∃ g ∈ B ∃ h ∈ C x = f G g G h
67 34 38 66 3bitr4rd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A F B F C ↔ x ∈ A F B F C
68 67 eqrdv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A F B F C = A F B F C
69 0npr ⊢ ¬ ∅ ∈ 𝑷
70 3 69 ndmovass ⊢ ¬ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A F B F C = A F B F C
71 68 70 pm2.61i ⊢ A F B F C = A F B F C