Theorem onprcf1acwevdlem1 36086

Description: Lemma for onprcf1acwevd 36088 and prconf1acwevd 36089. (Contributed by BTernaryTau, 10-Sep-2026.)

Hypothesis

Ref	Expression
onprcf1acwevdlem1.1	⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}

Assertion

Ref	Expression
onprcf1acwevdlem1	⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ∈ V)

Distinct variable groups:   𝑦,𝐴   𝑦,𝑊   𝑥,𝑟,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐴(𝑥, 𝑟)   𝐵(𝑟)   𝑊(𝑥, 𝑟)

Proof of Theorem onprcf1acwevdlem1

Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.28v 2031	. . . . 5 ⊢ (∀𝑦((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
2		df-ral 3081	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵)))
3	2	anbi2i 635	. . . . 5 ⊢ (((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
4	1, 3	bitr4i 281	. . . 4 ⊢ (∀𝑦((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)))
5		df-3an 1105	. . . . 5 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
6	5	albii 1852	. . . 4 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ∀𝑦((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
7		df-3an 1105	. . . 4 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)))
8	4, 6, 7	3bitr4ri 307	. . 3 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) ↔ ∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
9		nfa1 2191	. . . 4 ⊢ Ⅎ𝑦∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵)))
10		nfcv 2926	. . . 4 ⊢ Ⅎ𝑦𝐴
11		nfcv 2926	. . . 4 ⊢ Ⅎ𝑦{𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}
12		idd 25	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ⊆ 𝑊 → 𝐴 ⊆ 𝑊))
13		idd 25	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → (𝐵 ∈ On → 𝐵 ∈ On))
14		pm2.27 43	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵)) → ¬ 𝑦 We (𝑅1‘𝐵)))
15	12, 13, 14	3anim123d 1472	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵))))
16		simp1 1154	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ⊆ 𝑊)
17		ssel2 3908	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑊)
18		vex 3458	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
19		sseq1 3938	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑦 → (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ↔ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥))))
20		weeq1 5645	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑦 → (𝑟 We (𝑅1‘𝑥) ↔ 𝑦 We (𝑅1‘𝑥)))
21	19, 20	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ((𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥)) ↔ (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
22	21	rexbidv 3190	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑦 → (∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥)) ↔ ∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
23		onprcf1acwevdlem1.1	. . . . . . . . . . 11 ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}
24	18, 22, 23	elab2 3639	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑊 ↔ ∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)))
25	17, 24	sylib 221	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴) → ∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)))
26	25	expcom 419	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 → (𝐴 ⊆ 𝑊 → ∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
27	16, 26	syl5 35	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → ∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
28		ontri1 6423	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐵))
29	28	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑥 ∈ 𝐵 → 𝐵 ⊆ 𝑥))
30		r1ord3 9826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 → (𝑅1‘𝐵) ⊆ (𝑅1‘𝑥)))
31	30	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥) → (𝑅1‘𝐵) ⊆ (𝑅1‘𝑥))
32		wess 5644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅1‘𝐵) ⊆ (𝑅1‘𝑥) → (𝑦 We (𝑅1‘𝑥) → 𝑦 We (𝑅1‘𝐵)))
33	31, 32	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥) → (𝑦 We (𝑅1‘𝑥) → 𝑦 We (𝑅1‘𝐵)))
34	33	con3d 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥) → (¬ 𝑦 We (𝑅1‘𝐵) → ¬ 𝑦 We (𝑅1‘𝑥)))
35	34	3expia 1139	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 → (¬ 𝑦 We (𝑅1‘𝐵) → ¬ 𝑦 We (𝑅1‘𝑥))))
36	35	com23 87	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑦 We (𝑅1‘𝐵) → (𝐵 ⊆ 𝑥 → ¬ 𝑦 We (𝑅1‘𝑥))))
37	29, 36	syl5d 74	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑦 We (𝑅1‘𝐵) → (¬ 𝑥 ∈ 𝐵 → ¬ 𝑦 We (𝑅1‘𝑥))))
38	37	3impia 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (¬ 𝑥 ∈ 𝐵 → ¬ 𝑦 We (𝑅1‘𝑥)))
39	38	con4d 116	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (𝑦 We (𝑅1‘𝑥) → 𝑥 ∈ 𝐵))
40		simp1 1154	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐵 ∈ On)
41	39, 40	jctild 535	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (𝑦 We (𝑅1‘𝑥) → (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵)))
42	41	3expia 1139	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑦 We (𝑅1‘𝐵) → (𝑦 We (𝑅1‘𝑥) → (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵))))
43	42	impancom 457	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (𝑥 ∈ On → (𝑦 We (𝑅1‘𝑥) → (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵))))
44	43	imp 412	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) ∧ 𝑥 ∈ On) → (𝑦 We (𝑅1‘𝑥) → (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵)))
45	44	adantld 496	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) ∧ 𝑥 ∈ On) → ((𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵)))
46		r1ord2 9825	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
47	46	imp 412	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵))
48		fvex 6929	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝑥) ∈ V
49		sseq1 3938	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 ⊆ (𝑅1‘𝐵) ↔ (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
50		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑅1‘𝑥) → 𝑤 = (𝑅1‘𝑥))
51	50	sqxpeqd 5690	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 × 𝑤) = ((𝑅1‘𝑥) × (𝑅1‘𝑥)))
52	51	sseq2d 3945	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑦 ⊆ (𝑤 × 𝑤) ↔ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥))))
53		weeq2 5646	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑦 We 𝑤 ↔ 𝑦 We (𝑅1‘𝑥)))
54	49, 52, 53	3anbi123d 1465	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑅1‘𝑥) → ((𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤) ↔ ((𝑅1‘𝑥) ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
55	48, 54	spcev 3564	. . . . . . . . . . . . 13 ⊢ (((𝑅1‘𝑥) ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤))
56	55	3expib 1140	. . . . . . . . . . . 12 ⊢ ((𝑅1‘𝑥) ⊆ (𝑅1‘𝐵) → ((𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
57	47, 56	syl 18	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → ((𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
58	45, 57	syli 40	. . . . . . . . . 10 ⊢ (((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) ∧ 𝑥 ∈ On) → ((𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
59	58	rexlimdva 3167	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
60		sseq1 3938	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 ⊆ (𝑤 × 𝑤) ↔ 𝑦 ⊆ (𝑤 × 𝑤)))
61		weeq1 5645	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 We 𝑤 ↔ 𝑦 We 𝑤))
62	60, 61	3anbi23d 1468	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → ((𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ (𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
63	62	exbidv 1956	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
64	18, 63	elab 3636	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} ↔ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤))
65	59, 64	imbitrrdi 255	. . . . . . . 8 ⊢ ((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
66	65	3adant1 1148	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
67	27, 66	sylcom 31	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
68	15, 67	syldc 49	. . . . 5 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
69	68	sps 2225	. . . 4 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
70	9, 10, 11, 69	ssrd 3918	. . 3 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
71	8, 70	sylbi 220	. 2 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
72		fvex 6929	. . . 4 ⊢ (𝑅1‘𝐵) ∈ V
73		abweex 35842	. . . 4 ⊢ ((𝑅1‘𝐵) ∈ V → {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} ∈ V)
74	72, 73	ax-mp 5	. . 3 ⊢ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} ∈ V
75	74	ssex 5289	. 2 ⊢ (𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} → 𝐴 ∈ V)
76	71, 75	syl 18	1 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ∈ V)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  {cab 2741  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   We wwe 5610   × cxp 5656  Oncon0 6388  ‘cfv 6566  𝑅₁cr1 9803

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-r1 9805

This theorem is used by:  onprcf1acwevd  36088  prconf1acwevd  36089