Theorem onprcf1acwevdlem1 35996

Description: Lemma for onprcf1acwevd 35998 and prconf1acwevd 35999. (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 2028	. . . . 5 ⊢ (∀𝑦((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
2		df-ral 3077	. . . . . 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 1851	. . . 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 2187	. . . 4 ⊢ Ⅎ𝑦∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵)))
10		nfcv 2922	. . . 4 ⊢ Ⅎ𝑦𝐴
11		nfcv 2922	. . . 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 1471	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵))))
16		simp1 1154	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ⊆ 𝑊)
17		ssel2 3904	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑊)
18		vex 3454	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
19		sseq1 3934	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑦 → (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ↔ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥))))
20		weeq1 5638	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑦 → (𝑟 We (𝑅1‘𝑥) ↔ 𝑦 We (𝑅1‘𝑥)))
21	19, 20	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ((𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥)) ↔ (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
22	21	rexbidv 3186	. . . . . . . . . . 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 3635	. . . . . . . . . 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 6400	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐵))
29	28	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑥 ∈ 𝐵 → 𝐵 ⊆ 𝑥))
30		r1ord3 9796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 → (𝑅1‘𝐵) ⊆ (𝑅1‘𝑥)))
31	30	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥) → (𝑅1‘𝐵) ⊆ (𝑅1‘𝑥))
32		wess 5637	. . . . . . . . . . . . . . . . . . . . . . 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 9795	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
47	46	imp 412	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵))
48		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝑥) ∈ V
49		sseq1 3934	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 ⊆ (𝑅1‘𝐵) ↔ (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
50		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑅1‘𝑥) → 𝑤 = (𝑅1‘𝑥))
51	50	sqxpeqd 5683	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 × 𝑤) = ((𝑅1‘𝑥) × (𝑅1‘𝑥)))
52	51	sseq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑦 ⊆ (𝑤 × 𝑤) ↔ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥))))
53		weeq2 5639	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑦 We 𝑤 ↔ 𝑦 We (𝑅1‘𝑥)))
54	49, 52, 53	3anbi123d 1464	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑅1‘𝑥) → ((𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤) ↔ ((𝑅1‘𝑥) ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥))))
55	48, 54	spcev 3560	. . . . . . . . . . . . 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 3163	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
60		sseq1 3934	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 ⊆ (𝑤 × 𝑤) ↔ 𝑦 ⊆ (𝑤 × 𝑤)))
61		weeq1 5638	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 We 𝑤 ↔ 𝑦 We 𝑤))
62	60, 61	3anbi23d 1467	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → ((𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ (𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
63	62	exbidv 1953	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
64	18, 63	elab 3632	. . . . . . . . 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 2221	. . . 4 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
70	9, 10, 11, 69	ssrd 3914	. . 3 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
71	8, 70	sylbi 220	. 2 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
72		fvex 6903	. . . 4 ⊢ (𝑅1‘𝐵) ∈ V
73		abweex 35775	. . . 4 ⊢ ((𝑅1‘𝐵) ∈ V → {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} ∈ V)
74	72, 73	ax-mp 5	. . 3 ⊢ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)} ∈ V
75	74	ssex 5282	. 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 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3896   We wwe 5603   × cxp 5649  Oncon0 6365  ‘cfv 6543  𝑅₁cr1 9773

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-r1 9775

This theorem is used by:  onprcf1acwevd  35998  prconf1acwevd  35999