Theorem bropfvvvv 8093

Description: If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.)

Hypotheses

Ref	Expression
bropfvvvv.o	⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))
bropfvvvv.oo	⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})
bropfvvvv.s	⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆)
bropfvvvv.t	⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇)
bropfvvvv.p	⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
bropfvvvv	⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))

Distinct variable groups:   𝑈,𝑎   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒   𝑆,𝑎,𝑏,𝑐   𝑇,𝑎,𝑏,𝑐   𝜓,𝑎

Allowed substitution hints:   𝜑(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝜓(𝑒, 𝑏, 𝑐, 𝑑)   𝜃(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝐵(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝐶(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝐷(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑆(𝑒, 𝑑)   𝑇(𝑒, 𝑑)   𝑈(𝑒, 𝑏, 𝑐, 𝑑)   𝐸(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑂(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑉(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑊(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑋(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑌(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem bropfvvvv

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brovpreldm 8090	. 2 ⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴))
2		bropfvvvv.s	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆)
3		bropfvvvv.t	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇)
4		bropfvvvv.p	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
5	4	opabbidv 5175	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {⟨𝑑, 𝑒⟩ ∣ 𝜑} = {⟨𝑑, 𝑒⟩ ∣ 𝜓})
6	2, 3, 5	mpoeq123dv 7492	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
7		bropfvvvv.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))
8	6, 7	fvmptg 6988	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (𝑂‘𝐴) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
9	8	dmeqd 5893	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → dom (𝑂‘𝐴) = dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
10	9	eleq2d 2848	. . . . . 6 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓})))
11		dmoprabss 7521	. . . . . . . . 9 ⊢ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} ⊆ (𝑆 × 𝑇)
12	11	sseli 3930	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → ⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇))
13		bropfvvvv.oo	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})
14	7, 13	bropfvvvvlem 8092	. . . . . . . . 9 ⊢ ((⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))
15	14	ex 418	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
16	12, 15	syl 18	. . . . . . 7 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
17		df-mpo 7422	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
18	17	dmeqi 5892	. . . . . . 7 ⊢ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
19	16, 18	eleq2s 2880	. . . . . 6 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
20	10, 19	biimtrdi 256	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
21	20	com23 87	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
22	21	a1d 26	. . 3 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
23		ianor 997	. . . . 5 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) ↔ (¬ 𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V))
24	7	fvmptndm 7022	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ 𝑈 → (𝑂‘𝐴) = ∅)
25	24	dmeqd 5893	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ 𝑈 → dom (𝑂‘𝐴) = dom ∅)
26	25	eleq2d 2848	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom ∅))
27		dm0 5908	. . . . . . . . . 10 ⊢ dom ∅ = ∅
28	27	eleq2i 2854	. . . . . . . . 9 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom ∅ ↔ ⟨𝐵, 𝐶⟩ ∈ ∅)
29	26, 28	bitrdi 290	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ ∅))
30		noel 4287	. . . . . . . . 9 ⊢ ¬ ⟨𝐵, 𝐶⟩ ∈ ∅
31	30	pm2.21i 120	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
32	29, 31	biimtrdi 256	. . . . . . 7 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
33	32	a1d 26	. . . . . 6 ⊢ (¬ 𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
34		notnotb 318	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑈 ↔ ¬ ¬ 𝐴 ∈ 𝑈)
35		elex 3474	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑋 → 𝑆 ∈ V)
36		elex 3474	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ 𝑌 → 𝑇 ∈ V)
37	35, 36	anim12i 625	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
38	37	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
39		mpoexga 8080	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
40	38, 39	syl 18	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
41	40	pm2.24d 152	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
42	41	ex 418	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
43	42	com23 87	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
44	34, 43	sylbir 238	. . . . . . 7 ⊢ (¬ ¬ 𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
45	44	imp 412	. . . . . 6 ⊢ ((¬ ¬ 𝐴 ∈ 𝑈 ∧ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
46	33, 45	jaoi3 1076	. . . . 5 ⊢ ((¬ 𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
47	23, 46	sylbi 220	. . . 4 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
48	47	com34 92	. . 3 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
49	22, 48	pm2.61i 184	. 2 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
50	1, 49	mpdi 46	1 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  Vcvv 3453  ∅c0 4282  ⟨cop 4593   class class class wbr 5107  {copab 5171   ↦ cmpt 5190   × cxp 5657  dom cdm 5659  ‘cfv 6537  (class class class)co 7417  {coprab 7418   ∈ cmpo 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991

This theorem is used by:  wlkonprop  30124  wksonproplem  30174