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 𝐹 = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ( ( 𝑦Q𝑧Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
genpass.4 dom 𝐹 = ( P × P )
genpass.5 ( ( 𝑓P𝑔P ) → ( 𝑓 𝐹 𝑔 ) ∈ P )
genpass.6 ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) = ( 𝑓 𝐺 ( 𝑔 𝐺 ) )
Assertion genpass ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) )

Proof

Step Hyp Ref Expression
1 genp.1 𝐹 = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ( ( 𝑦Q𝑧Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 genpass.4 dom 𝐹 = ( P × P )
4 genpass.5 ( ( 𝑓P𝑔P ) → ( 𝑓 𝐹 𝑔 ) ∈ P )
5 genpass.6 ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) = ( 𝑓 𝐺 ( 𝑔 𝐺 ) )
6 1 2 genpelv ( ( 𝐵P𝐶P ) → ( 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) ↔ ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ) )
7 6 3adant1 ( ( 𝐴P𝐵P𝐶P ) → ( 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) ↔ ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ) )
8 7 anbi1d ( ( 𝐴P𝐵P𝐶P ) → ( ( 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ) )
9 8 exbidv ( ( 𝐴P𝐵P𝐶P ) → ( ∃ 𝑡 ( 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ∃ 𝑡 ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ) )
10 df-rex ( ∃ 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ↔ ∃ 𝑡 ( 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
11 ovex ( 𝑔 𝐺 ) ∈ V
12 11 isseti 𝑡 𝑡 = ( 𝑔 𝐺 )
13 12 biantrur ( 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ( ∃ 𝑡 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
14 19.41v ( ∃ 𝑡 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ( ∃ 𝑡 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
15 13 14 bitr4i ( 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
16 15 rexbii ( ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝐶𝑡 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
17 rexcom4 ( ∃ 𝐶𝑡 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ∃ 𝑡𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
18 16 17 bitri ( ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
19 18 rexbii ( ∃ 𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑔𝐵𝑡𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
20 rexcom4 ( ∃ 𝑔𝐵𝑡𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ∃ 𝑡𝑔𝐵𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
21 oveq2 ( 𝑡 = ( 𝑔 𝐺 ) → ( 𝑓 𝐺 𝑡 ) = ( 𝑓 𝐺 ( 𝑔 𝐺 ) ) )
22 21 5 eqtr4di ( 𝑡 = ( 𝑔 𝐺 ) → ( 𝑓 𝐺 𝑡 ) = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) )
23 22 eqeq2d ( 𝑡 = ( 𝑔 𝐺 ) → ( 𝑥 = ( 𝑓 𝐺 𝑡 ) ↔ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
24 23 pm5.32i ( ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
25 24 rexbii ( ∃ 𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ∃ 𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
26 r19.41v ( ∃ 𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ( ∃ 𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
27 25 26 bitr3i ( ∃ 𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ( ∃ 𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
28 27 rexbii ( ∃ 𝑔𝐵𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ∃ 𝑔𝐵 ( ∃ 𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
29 r19.41v ( ∃ 𝑔𝐵 ( ∃ 𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) ↔ ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
30 28 29 bitri ( ∃ 𝑔𝐵𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
31 30 exbii ( ∃ 𝑡𝑔𝐵𝐶 ( 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ∃ 𝑡 ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
32 19 20 31 3bitri ( ∃ 𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡 ( ∃ 𝑔𝐵𝐶 𝑡 = ( 𝑔 𝐺 ) ∧ 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
33 9 10 32 3bitr4g ( ( 𝐴P𝐵P𝐶P ) → ( ∃ 𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ↔ ∃ 𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
34 33 rexbidv ( ( 𝐴P𝐵P𝐶P ) → ( ∃ 𝑓𝐴𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ↔ ∃ 𝑓𝐴𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
35 4 caovcl ( ( 𝐵P𝐶P ) → ( 𝐵 𝐹 𝐶 ) ∈ P )
36 1 2 genpelv ( ( 𝐴P ∧ ( 𝐵 𝐹 𝐶 ) ∈ P ) → ( 𝑥 ∈ ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) ↔ ∃ 𝑓𝐴𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
37 35 36 sylan2 ( ( 𝐴P ∧ ( 𝐵P𝐶P ) ) → ( 𝑥 ∈ ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) ↔ ∃ 𝑓𝐴𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
38 37 3impb ( ( 𝐴P𝐵P𝐶P ) → ( 𝑥 ∈ ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) ↔ ∃ 𝑓𝐴𝑡 ∈ ( 𝐵 𝐹 𝐶 ) 𝑥 = ( 𝑓 𝐺 𝑡 ) ) )
39 4 caovcl ( ( 𝐴P𝐵P ) → ( 𝐴 𝐹 𝐵 ) ∈ P )
40 1 2 genpelv ( ( ( 𝐴 𝐹 𝐵 ) ∈ P𝐶P ) → ( 𝑥 ∈ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) ↔ ∃ 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
41 39 40 stoic3 ( ( 𝐴P𝐵P𝐶P ) → ( 𝑥 ∈ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) ↔ ∃ 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
42 1 2 genpelv ( ( 𝐴P𝐵P ) → ( 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ) )
43 42 3adant3 ( ( 𝐴P𝐵P𝐶P ) → ( 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ) )
44 43 anbi1d ( ( 𝐴P𝐵P𝐶P ) → ( ( 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ( ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ) )
45 44 exbidv ( ( 𝐴P𝐵P𝐶P ) → ( ∃ 𝑡 ( 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ∃ 𝑡 ( ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ) )
46 df-rex ( ∃ 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ↔ ∃ 𝑡 ( 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
47 19.41v ( ∃ 𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) ↔ ( ∃ 𝑡 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
48 oveq1 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) → ( 𝑡 𝐺 ) = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) )
49 48 eqeq2d ( 𝑡 = ( 𝑓 𝐺 𝑔 ) → ( 𝑥 = ( 𝑡 𝐺 ) ↔ 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
50 49 rexbidv ( 𝑡 = ( 𝑓 𝐺 𝑔 ) → ( ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ↔ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
51 50 pm5.32i ( ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
52 51 exbii ( ∃ 𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ∃ 𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
53 ovex ( 𝑓 𝐺 𝑔 ) ∈ V
54 53 isseti 𝑡 𝑡 = ( 𝑓 𝐺 𝑔 )
55 54 biantrur ( ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ( ∃ 𝑡 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
56 47 52 55 3bitr4ri ( ∃ 𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
57 56 rexbii ( ∃ 𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑔𝐵𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
58 rexcom4 ( ∃ 𝑔𝐵𝑡 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ∃ 𝑡𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
59 57 58 bitri ( ∃ 𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
60 59 rexbii ( ∃ 𝑓𝐴𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑓𝐴𝑡𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
61 rexcom4 ( ∃ 𝑓𝐴𝑡𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ∃ 𝑡𝑓𝐴𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
62 r19.41vv ( ∃ 𝑓𝐴𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ( ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
63 62 exbii ( ∃ 𝑡𝑓𝐴𝑔𝐵 ( 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) ↔ ∃ 𝑡 ( ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
64 60 61 63 3bitri ( ∃ 𝑓𝐴𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ↔ ∃ 𝑡 ( ∃ 𝑓𝐴𝑔𝐵 𝑡 = ( 𝑓 𝐺 𝑔 ) ∧ ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ) )
65 45 46 64 3bitr4g ( ( 𝐴P𝐵P𝐶P ) → ( ∃ 𝑡 ∈ ( 𝐴 𝐹 𝐵 ) ∃ 𝐶 𝑥 = ( 𝑡 𝐺 ) ↔ ∃ 𝑓𝐴𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
66 41 65 bitrd ( ( 𝐴P𝐵P𝐶P ) → ( 𝑥 ∈ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) ↔ ∃ 𝑓𝐴𝑔𝐵𝐶 𝑥 = ( ( 𝑓 𝐺 𝑔 ) 𝐺 ) ) )
67 34 38 66 3bitr4rd ( ( 𝐴P𝐵P𝐶P ) → ( 𝑥 ∈ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) ) )
68 67 eqrdv ( ( 𝐴P𝐵P𝐶P ) → ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) )
69 0npr ¬ ∅ ∈ P
70 3 69 ndmovass ( ¬ ( 𝐴P𝐵P𝐶P ) → ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) )
71 68 70 pm2.61i ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) )