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

Metamath Proof Explorer

Theorem oemapval

Description: Value of the relation T . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
Assertion oemapval ( 𝜑 → ( 𝐹 𝑇 𝐺 ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6 oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
7 fveq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
8 fveq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
9 eleq12 ⊢ ( ( ( 𝑥 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑦 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ) )
11 fveq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
12 fveq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
13 11 12 eqeqan12d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
14 13 imbi2d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
15 14 ralbidv ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
16 10 15 anbi12d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )
17 16 rexbidv ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )
18 17 4 brabga ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐹 𝑇 𝐺 ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )
19 5 6 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 𝑇 𝐺 ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )