Metamath Proof Explorer

Theorem onprcf1acwevdlem1

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

Ref Expression
Hypothesis onprcf1acwevdlem1.1 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
Assertion onprcf1acwevdlem1 ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 onprcf1acwevdlem1.1 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
2 19.28v ⊢ ( ∀ 𝑦 ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
3 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
4 3 anbi2i ⊢ ( ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
5 2 4 bitr4i ⊢ ( ∀ 𝑦 ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
6 df-3an ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
7 6 albii ⊢ ( ∀ 𝑦 ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
8 df-3an ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
9 5 7 8 3bitr4ri ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ↔ ∀ 𝑦 ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
10 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
11 nfcv ⊢ Ⅎ 𝑦 𝐴
12 nfcv ⊢ Ⅎ 𝑦 { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) }
13 idd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ⊆ 𝑊 → 𝐴 ⊆ 𝑊 ) )
14 idd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐵 ∈ On → 𝐵 ∈ On ) )
15 pm2.27 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
16 13 14 15 3anim123d ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) → ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) )
17 simp1 ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝐴 ⊆ 𝑊 )
18 ssel2 ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝑊 )
19 vex ⊢ 𝑦 ∈ V
20 sseq1 ⊢ ( 𝑟 = 𝑦 → ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ↔ 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ) )
21 weeq1 ⊢ ( 𝑟 = 𝑦 → ( 𝑟 We ( 𝑅1 ‘ 𝑥 ) ↔ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
22 20 21 anbi12d ⊢ ( 𝑟 = 𝑦 → ( ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
23 22 rexbidv ⊢ ( 𝑟 = 𝑦 → ( ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
24 19 23 1 elab2 ⊢ ( 𝑦 ∈ 𝑊 ↔ ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
25 18 24 sylib ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
26 25 expcom ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ⊆ 𝑊 → ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
27 17 26 syl5 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
28 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐵 ) )
29 28 biimprd ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑥 ∈ 𝐵 → 𝐵 ⊆ 𝑥 ) )
30 r1ord3 ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 ⊆ 𝑥 → ( 𝑅1 ‘ 𝐵 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
31 30 3impia ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥 ) → ( 𝑅1 ‘ 𝐵 ) ⊆ ( 𝑅1 ‘ 𝑥 ) )
32 wess ⊢ ( ( 𝑅1 ‘ 𝐵 ) ⊆ ( 𝑅1 ‘ 𝑥 ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
33 31 32 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥 ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
34 33 con3d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ⊆ 𝑥 ) → ( ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) → ¬ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
35 34 3expia ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 ⊆ 𝑥 → ( ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) → ¬ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
36 35 com23 ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) → ( 𝐵 ⊆ 𝑥 → ¬ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
37 29 36 syl5d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐵 → ¬ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
38 37 3impia ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( ¬ 𝑥 ∈ 𝐵 → ¬ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
39 38 con4d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → 𝑥 ∈ 𝐵 ) )
40 simp1 ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝐵 ∈ On )
41 39 40 jctild ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) )
42 41 3expia ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) ) )
43 42 impancom ⊢ ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( 𝑥 ∈ On → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) ) )
44 43 imp ⊢ ( ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑥 ∈ On ) → ( 𝑦 We ( 𝑅1 ‘ 𝑥 ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) )
45 44 adantld ⊢ ( ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑥 ∈ On ) → ( ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) )
46 r1ord2 ⊢ ( 𝐵 ∈ On → ( 𝑥 ∈ 𝐵 → ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
47 46 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) )
48 fvex ⊢ ( 𝑅1 ‘ 𝑥 ) ∈ V
49 sseq1 ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
50 id ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → 𝑤 = ( 𝑅1 ‘ 𝑥 ) )
51 50 sqxpeqd ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → ( 𝑤 × 𝑤 ) = ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) )
52 51 sseq2d ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → ( 𝑦 ⊆ ( 𝑤 × 𝑤 ) ↔ 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ) )
53 weeq2 ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → ( 𝑦 We 𝑤 ↔ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) )
54 49 52 53 3anbi123d ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑥 ) → ( ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ↔ ( ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) ) )
55 48 54 spcev ⊢ ( ( ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) )
56 55 3expib ⊢ ( ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐵 ) → ( ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
57 47 56 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
58 45 57 syli ⊢ ( ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑥 ∈ On ) → ( ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
59 58 rexlimdva ⊢ ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
60 sseq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 ⊆ ( 𝑤 × 𝑤 ) ↔ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ) )
61 weeq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 We 𝑤 ↔ 𝑦 We 𝑤 ) )
62 60 61 3anbi23d ⊢ ( 𝑣 = 𝑦 → ( ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) ↔ ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
63 62 exbidv ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) ↔ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) ) )
64 19 63 elab ⊢ ( 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ↔ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑦 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑦 We 𝑤 ) )
65 59 64 imbitrrdi ⊢ ( ( 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ) )
66 65 3adant1 ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ On ( 𝑦 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑦 We ( 𝑅1 ‘ 𝑥 ) ) → 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ) )
67 27 66 sylcom ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ) )
68 16 67 syldc ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ) )
69 68 sps ⊢ ( ∀ 𝑦 ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ) )
70 10 11 12 69 ssrd ⊢ ( ∀ 𝑦 ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) ) → 𝐴 ⊆ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } )
71 9 70 sylbi ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝐴 ⊆ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } )
72 fvex ⊢ ( 𝑅1 ‘ 𝐵 ) ∈ V
73 abweex ⊢ ( ( 𝑅1 ‘ 𝐵 ) ∈ V → { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ∈ V )
74 72 73 ax-mp ⊢ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } ∈ V
75 74 ssex ⊢ ( 𝐴 ⊆ { 𝑣 ∣ ∃ 𝑤 ( 𝑤 ⊆ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑣 ⊆ ( 𝑤 × 𝑤 ) ∧ 𝑣 We 𝑤 ) } → 𝐴 ∈ V )
76 71 75 syl ⊢ ( ( 𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) → 𝐴 ∈ V )