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