Metamath Proof Explorer


Theorem adjeu

Description: Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion adjeu ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ∈ dom adj ↔ ∃! 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex ℋ ∈ V
2 fex2 ( ( 𝑇 : ℋ ⟶ ℋ ∧ ℋ ∈ V ∧ ℋ ∈ V ) → 𝑇 ∈ V )
3 1 1 2 mp3an23 ( 𝑇 : ℋ ⟶ ℋ → 𝑇 ∈ V )
4 feq1 ( 𝑡 = 𝑇 → ( 𝑡 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ ℋ ) )
5 fveq1 ( 𝑡 = 𝑇 → ( 𝑡𝑦 ) = ( 𝑇𝑦 ) )
6 5 oveq2d ( 𝑡 = 𝑇 → ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( 𝑥 ·ih ( 𝑇𝑦 ) ) )
7 6 eqeq1d ( 𝑡 = 𝑇 → ( ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
8 7 2ralbidv ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
9 4 8 3anbi13d ( 𝑡 = 𝑇 → ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
10 3anass ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
11 9 10 bitrdi ( 𝑡 = 𝑇 → ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) ) )
12 11 exbidv ( 𝑡 = 𝑇 → ( ∃ 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ∃ 𝑢 ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) ) )
13 19.42v ( ∃ 𝑢 ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
14 12 13 bitrdi ( 𝑡 = 𝑇 → ( ∃ 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) ) )
15 dfadj2 adj = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) }
16 15 dmeqi dom adj = dom { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) }
17 dmopab dom { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) } = { 𝑡 ∣ ∃ 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) }
18 16 17 eqtri dom adj = { 𝑡 ∣ ∃ 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) }
19 14 18 elab2g ( 𝑇 ∈ V → ( 𝑇 ∈ dom adj ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) ) )
20 19 baibd ( ( 𝑇 ∈ V ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑇 ∈ dom adj ↔ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
21 3 20 mpancom ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ∈ dom adj ↔ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
22 df-reu ( ∃! 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ↔ ∃! 𝑢 ( 𝑢 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
23 1 1 elmap ( 𝑢 ∈ ( ℋ ↑m ℋ ) ↔ 𝑢 : ℋ ⟶ ℋ )
24 23 anbi1i ( ( 𝑢 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
25 24 eubii ( ∃! 𝑢 ( 𝑢 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ∃! 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
26 adjmo ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) )
27 df-eu ( ∃! 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ( ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ∧ ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ) )
28 26 27 mpbiran2 ( ∃! 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) ↔ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
29 22 25 28 3bitri ( ∃! 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )
30 21 29 bitr4di ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ∈ dom adj ↔ ∃! 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑢𝑥 ) ·ih 𝑦 ) ) )