Theorem bropfvvvv 8075

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 8072	. 2 ⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴))
2		bropfvvvv.s	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆)
3		bropfvvvv.t	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇)
4		bropfvvvv.p	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
5	4	opabbidv 5171	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {⟨𝑑, 𝑒⟩ ∣ 𝜑} = {⟨𝑑, 𝑒⟩ ∣ 𝜓})
6	2, 3, 5	mpoeq123dv 7475	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
7		bropfvvvv.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))
8	6, 7	fvmptg 6977	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (𝑂‘𝐴) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
9	8	dmeqd 5886	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → dom (𝑂‘𝐴) = dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}))
10	9	eleq2d 2851	. . . . . 6 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓})))
11		dmoprabss 7504	. . . . . . . . 9 ⊢ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} ⊆ (𝑆 × 𝑇)
12	11	sseli 3935	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → ⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇))
13		bropfvvvv.oo	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})
14	7, 13	bropfvvvvlem 8074	. . . . . . . . 9 ⊢ ((⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))
15	14	ex 417	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
16	12, 15	syl 18	. . . . . . 7 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})} → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
17		df-mpo 7405	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
18	17	dmeqi 5885	. . . . . . 7 ⊢ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) = dom {⟨⟨𝑏, 𝑐⟩, 𝑧⟩ ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {⟨𝑑, 𝑒⟩ ∣ 𝜓})}
19	16, 18	eleq2s 2883	. . . . . 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 7011	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ 𝑈 → (𝑂‘𝐴) = ∅)
25	24	dmeqd 5886	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ 𝑈 → dom (𝑂‘𝐴) = dom ∅)
26	25	eleq2d 2851	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ dom ∅))
27		dm0 5901	. . . . . . . . . 10 ⊢ dom ∅ = ∅
28	27	eleq2i 2857	. . . . . . . . 9 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom ∅ ↔ ⟨𝐵, 𝐶⟩ ∈ ∅)
29	26, 28	bitrdi 290	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ 𝑈 → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) ↔ ⟨𝐵, 𝐶⟩ ∈ ∅))
30		noel 4293	. . . . . . . . 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 3478	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑋 → 𝑆 ∈ V)
36		elex 3478	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ 𝑌 → 𝑇 ∈ V)
37	35, 36	anim12i 624	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
38	37	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
39		mpoexga 8062	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
40	38, 39	syl 18	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V)
41	40	pm2.24d 152	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
42	41	ex 417	. . . . . . . . 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 411	. . . . . 6 ⊢ ((¬ ¬ 𝐴 ∈ 𝑈 ∧ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (⟨𝐵, 𝐶⟩ ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))
46	33, 45	jaoi3 1074	. . . . 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))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ∅c0 4288  ⟨cop 4591   class class class wbr 5105  {copab 5167   ↦ cmpt 5186   × cxp 5650  dom cdm 5652  ‘cfv 6525  (class class class)co 7400  {coprab 7401   ∈ cmpo 7402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975

This theorem is referenced by:  wlkonprop  29915  wksonproplem  29961