Theorem onprcf1acwevdlem1 35895

Description: Lemma for onprcf1acwevd 35897. (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 2029	. . . . 5 ⊢ (∀𝑦((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) ↔ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On) ∧ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))))
2		df-ral 3078	. . . . . 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 2188	. . . 4 ⊢ Ⅎ𝑦∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵)))
10		nfcv 2923	. . . 4 ⊢ Ⅎ𝑦𝐴
11		nfcv 2923	. . . 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 3926	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑊)
18		vex 3455	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
19		sseq1 3956	. . . . . . . . . . . . 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 3187	. . . . . . . . . . 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 3636	. . . . . . . . . 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 6397	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐵))
29	28	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑥 ∈ 𝐵 → 𝐵 ⊆ 𝑥))
30		r1ord3 9789	. . . . . . . . . . . . . . . . . . . . . . . 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 9788	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
47	46	imp 412	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵))
48		fvex 6898	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝑥) ∈ V
49		sseq1 3956	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 ⊆ (𝑅1‘𝐵) ↔ (𝑅1‘𝑥) ⊆ (𝑅1‘𝐵)))
50		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝑅1‘𝑥) → 𝑤 = (𝑅1‘𝑥))
51	50	sqxpeqd 5683	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑅1‘𝑥) → (𝑤 × 𝑤) = ((𝑅1‘𝑥) × (𝑅1‘𝑥)))
52	51	sseq2d 3963	. . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . 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 3164	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ ¬ 𝑦 We (𝑅1‘𝐵)) → (∃𝑥 ∈ On (𝑦 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑦 We (𝑅1‘𝑥)) → ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
60		sseq1 3956	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 ⊆ (𝑤 × 𝑤) ↔ 𝑦 ⊆ (𝑤 × 𝑤)))
61		weeq1 5638	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑦 → (𝑣 We 𝑤 ↔ 𝑦 We 𝑤))
62	60, 61	3anbi23d 1467	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → ((𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ (𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
63	62	exbidv 1954	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤) ↔ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑦 ⊆ (𝑤 × 𝑤) ∧ 𝑦 We 𝑤)))
64	18, 63	elab 3633	. . . . . . . . 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 2222	. . . 4 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)}))
70	9, 10, 11, 69	ssrd 3936	. . 3 ⊢ (∀𝑦(𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 We (𝑅1‘𝐵))) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
71	8, 70	sylbi 220	. 2 ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ⊆ {𝑣 ∣ ∃𝑤(𝑤 ⊆ (𝑅1‘𝐵) ∧ 𝑣 ⊆ (𝑤 × 𝑤) ∧ 𝑣 We 𝑤)})
72		fvex 6898	. . . 4 ⊢ (𝑅1‘𝐵) ∈ V
73		abweex 35718	. . . 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 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ⊆ wss 3899   We wwe 5603   × cxp 5649  Oncon0 6362  ‘cfv 6538  𝑅₁cr1 9766

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 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  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 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-r1 9768

This theorem is used by:  onprcf1acwevd  35897