Theorem bropfvvvv 8116

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 8113	. 2 ⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴))
2		bropfvvvv.s	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆)
3		bropfvvvv.t	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇)
4		bropfvvvv.p	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
5	4	opabbidv 5214	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {⟨𝑑, 𝑒⟩ ∣ 𝜑} = {⟨𝑑, 𝑒⟩ ∣ 𝜓})
6	2, 3, 5	mpoeq123dv 7508	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
7		bropfvvvv.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))
8	6, 7	fvmptg 7014	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (𝑂‘𝐴) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
9	8	dmeqd 5919	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → dom (𝑂‘𝐴) = dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
10	9	eleq2d 2825	. . . . . 6 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓})))
11		dmoprabss 7536	. . . . . . . . 9 ⊢ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} ⊆ (𝑆 × 𝑇)
12	11	sseli 3991	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → ⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇))
13		bropfvvvv.oo	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})
14	7, 13	bropfvvvvlem 8115	. . . . . . . . 9 ⊢ ((⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))
15	14	ex 412	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
16	12, 15	syl 17	. . . . . . 7 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
17		df-mpo 7436	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
18	17	dmeqi 5918	. . . . . . 7 ⊢ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
19	16, 18	eleq2s 2857	. . . . . 6 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
20	10, 19	biimtrdi 253	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
21	20	com23 86	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
22	21	a1d 25	. . 3 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
23		ianor 983	. . . . 5 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) ↔ (¬ 𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V))
24	7	fvmptndm 7047	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ 𝑈 → (𝑂‘𝐴) = ∅)
25	24	dmeqd 5919	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ 𝑈 → dom (𝑂‘𝐴) = dom ∅)
26	25	eleq2d 2825	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom ∅))
27		dm0 5934	. . . . . . . . . 10 ⊢ dom ∅ = ∅
28	27	eleq2i 2831	. . . . . . . . 9 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom ∅ ↔ ⟨𝐵, 𝐶⟩ ∈ ∅)
29	26, 28	bitrdi 287	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ ∅))
30		noel 4344	. . . . . . . . 9 ⊢ ¬ ⟨𝐵, 𝐶⟩ ∈ ∅
31	30	pm2.21i 119	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
32	29, 31	biimtrdi 253	. . . . . . 7 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
33	32	a1d 25	. . . . . 6 ⊢ (¬ 𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
34		notnotb 315	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑈 ↔ ¬ ¬ 𝐴 ∈ 𝑈)
35		elex 3499	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑋 → 𝑆 ∈ V)
36		elex 3499	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ 𝑌 → 𝑇 ∈ V)
37	35, 36	anim12i 613	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
38	37	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
39		mpoexga 8101	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
41	40	pm2.24d 151	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
42	41	ex 412	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
43	42	com23 86	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
44	34, 43	sylbir 235	. . . . . . 7 ⊢ (¬ ¬ 𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))))
45	44	imp 406	. . . . . 6 ⊢ ((¬ ¬ 𝐴 ∈ 𝑈 ∧ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
46	33, 45	jaoi3 1060	. . . . 5 ⊢ ((¬ 𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
47	23, 46	sylbi 217	. . . 4 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
48	47	com34 91	. . 3 ⊢ (¬ (𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
49	22, 48	pm2.61i 182	. 2 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))
50	1, 49	mpdi 45	1 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  Vcvv 3478  ∅c0 4339  ⟨cop 4637   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   × cxp 5687  dom cdm 5689  ‘cfv 6563  (class class class)co 7431  {coprab 7432   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014

This theorem is referenced by:  wlkonprop  29691  wksonproplem  29737  wksonproplemOLD  29738