This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) )