Metamath Proof Explorer

Theorem frmin

Description: Every (possibly proper) subclass of a class A with a well-founded set-like relation R has a minimal element. This is a very strong generalization of tz6.26 and tz7.5 . (Contributed by Scott Fenton, 4-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 27-Nov-2024)

Ref Expression
Assertion frmin ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )

Proof

Step Hyp Ref Expression
1 frss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Fr 𝐴 → 𝑅 Fr 𝐵 ) )
2 sess2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Se 𝐴 → 𝑅 Se 𝐵 ) )
3 1 2 anim12d ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ) )
4 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐵 )
5 predeq3 ⊢ ( 𝑦 = 𝑏 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐵 , 𝑏 ) )
6 5 eqeq1d ⊢ ( 𝑦 = 𝑏 → ( Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ ) )
7 6 rspcev ⊢ ( ( 𝑏 ∈ 𝐵 ∧ Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )
8 7 ex ⊢ ( 𝑏 ∈ 𝐵 → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
9 8 adantl ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
10 predres ⊢ Pred ( 𝑅 , 𝐵 , 𝑏 ) = Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 )
11 relres ⊢ Rel ( 𝑅 ↾ 𝐵 )
12 ssttrcl ⊢ ( Rel ( 𝑅 ↾ 𝐵 ) → ( 𝑅 ↾ 𝐵 ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) )
13 11 12 ax-mp ⊢ ( 𝑅 ↾ 𝐵 ) ⊆ t++ ( 𝑅 ↾ 𝐵 )
14 predrelss ⊢ ( ( 𝑅 ↾ 𝐵 ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) → Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) )
15 13 14 ax-mp ⊢ Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 )
16 10 15 eqsstri ⊢ Pred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 )
17 ssn0 ⊢ ( ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∧ Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ )
18 16 17 mpan ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ )
19 predss ⊢ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵
20 18 19 jctil ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) )
21 dffr4 ⊢ ( 𝑅 Fr 𝐵 ↔ ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) )
22 21 biimpi ⊢ ( 𝑅 Fr 𝐵 → ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) )
23 ttrclse ⊢ ( 𝑅 Se 𝐵 → t++ ( 𝑅 ↾ 𝐵 ) Se 𝐵 )
24 setlikespec ⊢ ( ( 𝑏 ∈ 𝐵 ∧ t++ ( 𝑅 ↾ 𝐵 ) Se 𝐵 ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∈ V )
25 23 24 sylan2 ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∈ V )
26 25 ancoms ⊢ ( ( 𝑅 Se 𝐵 ∧ 𝑏 ∈ 𝐵 ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∈ V )
27 sseq1 ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( 𝑐 ⊆ 𝐵 ↔ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ) )
28 neeq1 ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( 𝑐 ≠ ∅ ↔ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) )
29 27 28 anbi12d ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) ↔ ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) ) )
30 predeq2 ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → Pred ( 𝑅 , 𝑐 , 𝑦 ) = Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) )
31 30 eqeq1d ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
32 31 rexeqbi1dv ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
33 29 32 imbi12d ⊢ ( 𝑐 = Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) → ( ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) ↔ ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) ) )
34 33 spcgv ⊢ ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∈ V → ( ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) → ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) ) )
35 34 impcom ⊢ ( ( ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∈ V ) → ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
36 22 26 35 syl2an ⊢ ( ( 𝑅 Fr 𝐵 ∧ ( 𝑅 Se 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
37 36 anassrs ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
38 predres ⊢ Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 )
39 predrelss ⊢ ( ( 𝑅 ↾ 𝐵 ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) → Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 ) )
40 13 39 ax-mp ⊢ Pred ( ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 )
41 38 40 eqsstri ⊢ Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 )
42 inss1 ⊢ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 )
43 coss1 ⊢ ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) → ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
44 42 43 ax-mp ⊢ ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) )
45 coss2 ⊢ ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) → ( t++ ( 𝑅 ↾ 𝐵 ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ t++ ( 𝑅 ↾ 𝐵 ) ) )
46 42 45 ax-mp ⊢ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ t++ ( 𝑅 ↾ 𝐵 ) )
47 44 46 sstri ⊢ ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ t++ ( 𝑅 ↾ 𝐵 ) )
48 ttrcltr ⊢ ( t++ ( 𝑅 ↾ 𝐵 ) ∘ t++ ( 𝑅 ↾ 𝐵 ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 )
49 47 48 sstri ⊢ ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 )
50 predtrss ⊢ ( ( ( ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ) ⊆ t++ ( 𝑅 ↾ 𝐵 ) ∧ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∧ 𝑏 ∈ 𝐵 ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) )
51 49 50 mp3an1 ⊢ ( ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∧ 𝑏 ∈ 𝐵 ) → Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) )
52 41 51 sstrid ⊢ ( ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) )
53 sspred ⊢ ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) )
54 19 52 53 sylancr ⊢ ( ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) )
55 54 ancoms ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) )
56 55 eqeq1d ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ) → ( Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
57 56 rexbidva ⊢ ( 𝑏 ∈ 𝐵 → ( ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
58 ssrexv ⊢ ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 → ( ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
59 19 58 ax-mp ⊢ ( ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )
60 57 59 biimtrrdi ⊢ ( 𝑏 ∈ 𝐵 → ( ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
61 60 adantl ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) Pred ( 𝑅 , Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
62 37 61 syld ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( t++ ( 𝑅 ↾ 𝐵 ) , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
63 20 62 syl5 ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
64 9 63 pm2.61dne ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )
65 64 ex ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( 𝑏 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
66 65 exlimdv ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( ∃ 𝑏 𝑏 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
67 4 66 biimtrid ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( 𝐵 ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
68 3 67 syl6com ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐵 ⊆ 𝐴 → ( 𝐵 ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) ) )
69 68 imp32 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )