Metamath Proof Explorer

Theorem oemapval

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

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
oemapval.f ⊢ φ → F ∈ S
oemapval.g ⊢ φ → G ∈ S
Assertion oemapval ⊢ φ → F T G ↔ ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 oemapval.f ⊢ φ → F ∈ S
6 oemapval.g ⊢ φ → G ∈ S
7 fveq1 ⊢ x = F → x ⁡ z = F ⁡ z
8 fveq1 ⊢ y = G → y ⁡ z = G ⁡ z
9 eleq12 ⊢ x ⁡ z = F ⁡ z ∧ y ⁡ z = G ⁡ z → x ⁡ z ∈ y ⁡ z ↔ F ⁡ z ∈ G ⁡ z
10 7 8 9 syl2an ⊢ x = F ∧ y = G → x ⁡ z ∈ y ⁡ z ↔ F ⁡ z ∈ G ⁡ z
11 fveq1 ⊢ x = F → x ⁡ w = F ⁡ w
12 fveq1 ⊢ y = G → y ⁡ w = G ⁡ w
13 11 12 eqeqan12d ⊢ x = F ∧ y = G → x ⁡ w = y ⁡ w ↔ F ⁡ w = G ⁡ w
14 13 imbi2d ⊢ x = F ∧ y = G → z ∈ w → x ⁡ w = y ⁡ w ↔ z ∈ w → F ⁡ w = G ⁡ w
15 14 ralbidv ⊢ x = F ∧ y = G → ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w ↔ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
16 10 15 anbi12d ⊢ x = F ∧ y = G → x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w ↔ F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
17 16 rexbidv ⊢ x = F ∧ y = G → ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w ↔ ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
18 17 4 brabga ⊢ F ∈ S ∧ G ∈ S → F T G ↔ ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w
19 5 6 18 syl2anc ⊢ φ → F T G ↔ ∃ z ∈ B F ⁡ z ∈ G ⁡ z ∧ ∀ w ∈ B z ∈ w → F ⁡ w = G ⁡ w