Theorem oprabex3

Description: Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004)

	Ref	Expression
Hypotheses	oprabex3.1	⊢ 𝐻 ∈ V
	oprabex3.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
Assertion	oprabex3	⊢ 𝐹 ∈ V

Proof

Step	Hyp	Ref	Expression
1		oprabex3.1	⊢ 𝐻 ∈ V
2		oprabex3.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ) }
3	1 1	xpex	⊢ ( 𝐻 × 𝐻 ) ∈ V
4		moeq	⊢ ∃* 𝑧 𝑧 = 𝑅
5	4	mosubop	⊢ ∃* 𝑧 ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 )
6	5	mosubop	⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) )
7		anass	⊢ ( ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
8	7	2exbii	⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
9		19.42vv	⊢ ( ∃ 𝑢 ∃ 𝑓 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
10	8 9	bitri	⊢ ( ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
11	10	2exbii	⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
12	11	mobii	⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) ↔ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ ∃ 𝑢 ∃ 𝑓 ( 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ∧ 𝑧 = 𝑅 ) ) )
13	6 12	mpbir	⊢ ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 )
14	13	a1i	⊢ ( ( 𝑥 ∈ ( 𝐻 × 𝐻 ) ∧ 𝑦 ∈ ( 𝐻 × 𝐻 ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = 𝑅 ) )
15	3 3 14 2	oprabex	⊢ 𝐹 ∈ V