Metamath Proof Explorer

Theorem onprcf1acwevdlem2

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

Ref Expression
Hypotheses onprcf1acwevdlem2.1 ⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
onprcf1acwevdlem2.2 ⊢ 𝑆 = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
onprcf1acwevdlem2.3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ On ) → ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) )
Assertion onprcf1acwevdlem2 ( 𝜑 → 𝑅 We V )

Proof

Step Hyp Ref Expression
1 onprcf1acwevdlem2.1 ⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
2 onprcf1acwevdlem2.2 ⊢ 𝑆 = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
3 onprcf1acwevdlem2.3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ On ) → ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) )
4 rankon ⊢ ( rank ‘ 𝑦 ) ∈ On
5 4 onsuci ⊢ suc ( rank ‘ 𝑦 ) ∈ On
6 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ On ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) )
7 eqidd ⊢ ( 𝑢 = suc ( rank ‘ 𝑦 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
8 fveq2 ⊢ ( 𝑢 = suc ( rank ‘ 𝑦 ) → ( 𝑅1 ‘ 𝑢 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
9 7 8 weeq12d ⊢ ( 𝑢 = suc ( rank ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) ↔ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
10 9 rexbidv ⊢ ( 𝑢 = suc ( rank ‘ 𝑦 ) → ( ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) ↔ ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
11 10 rspcv ⊢ ( suc ( rank ‘ 𝑦 ) ∈ On → ( ∀ 𝑢 ∈ On ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑢 ) → ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
12 5 6 11 mpsyl ⊢ ( 𝜑 → ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
13 12 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
14 vex ⊢ 𝑣 ∈ V
15 14 rankr1 ⊢ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑣 ) ↔ ( ¬ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑦 ) ) ∧ 𝑣 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
16 15 simprbi ⊢ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑣 ) → 𝑣 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
17 16 eqcoms ⊢ ( ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) → 𝑣 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
18 17 rgenw ⊢ ∀ 𝑣 ∈ V ( ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) → 𝑣 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
19 rabss ⊢ ( { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑣 ∈ V ( ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) → 𝑣 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
20 18 19 mpbir ⊢ { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) )
21 nfcv ⊢ Ⅎ 𝑤 𝐹
22 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) }
23 22 nfint ⊢ Ⅎ 𝑤 ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) }
24 21 23 nffv ⊢ Ⅎ 𝑤 ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
25 2 24 nfcxfr ⊢ Ⅎ 𝑤 𝑆
26 nfcv ⊢ Ⅎ 𝑤 ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) )
27 25 26 nfwe ⊢ Ⅎ 𝑤 𝑆 We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) )
28 fveq2 ⊢ ( 𝑤 = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) )
29 28 2 eqtr4di ⊢ ( 𝑤 = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } → ( 𝐹 ‘ 𝑤 ) = 𝑆 )
30 eqidd ⊢ ( 𝑤 = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
31 29 30 weeq12d ⊢ ( 𝑤 = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } → ( ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ↔ 𝑆 We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
32 27 31 onminsb ⊢ ( ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → 𝑆 We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
33 wess ⊢ ( { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → ( 𝑆 We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } ) )
34 20 32 33 mpsyl ⊢ ( ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } )
35 34 alimi ⊢ ( ∀ 𝑦 ∃ 𝑤 ∈ On ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → ∀ 𝑦 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } )
36 ralv ⊢ ( ∀ 𝑦 ∈ V 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } ↔ ∀ 𝑦 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } )
37 eqidd ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
38 suceq ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → suc 𝑞 = suc ( rank ‘ 𝑦 ) )
39 38 fveq2d ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ( 𝑅1 ‘ suc 𝑞 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
40 37 39 weeq12d ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc 𝑞 ) ↔ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
41 40 rabbidv ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc 𝑞 ) } = { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
42 41 inteqd ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc 𝑞 ) } = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
43 42 fveq2d ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc 𝑞 ) } ) = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) )
44 43 2 eqtr4di ⊢ ( 𝑞 = ( rank ‘ 𝑦 ) → ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc 𝑞 ) } ) = 𝑆 )
45 eqidd ⊢ ( 𝑡 = 𝑦 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
46 fveq2 ⊢ ( 𝑡 = 𝑦 → ( rank ‘ 𝑡 ) = ( rank ‘ 𝑦 ) )
47 46 suceqd ⊢ ( 𝑡 = 𝑦 → suc ( rank ‘ 𝑡 ) = suc ( rank ‘ 𝑦 ) )
48 47 fveq2d ⊢ ( 𝑡 = 𝑦 → ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
49 45 48 weeq12d ⊢ ( 𝑡 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) ↔ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) )
50 49 rabbidv ⊢ ( 𝑡 = 𝑦 → { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) } = { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
51 50 inteqd ⊢ ( 𝑡 = 𝑦 → ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) } = ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
52 51 fveq2d ⊢ ( 𝑡 = 𝑦 → ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) } ) = ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } ) )
53 52 2 eqtr4di ⊢ ( 𝑡 = 𝑦 → ( 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑡 ) ) } ) = 𝑆 )
54 1 44 53 werankwe ⊢ ( ∀ 𝑦 ∈ V 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } → 𝑅 We V )
55 36 54 sylbir ⊢ ( ∀ 𝑦 𝑆 We { 𝑣 ∈ V ∣ ( rank ‘ 𝑣 ) = ( rank ‘ 𝑦 ) } → 𝑅 We V )
56 13 35 55 3syl ⊢ ( 𝜑 → 𝑅 We V )