# 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 ( 𝜑 → ( 𝐹 𝑇 𝐺 ↔ ∃ 𝑧𝐵 ( ( 𝐹𝑧 ) ∈ ( 𝐺𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ) ) ) )