Metamath Proof Explorer

Theorem wfrlem10OLD

Description: Lemma for well-ordered recursion. When z is an R minimal element of ( A \ dom F ) , then its predecessor class is equal to dom F . Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem10OLD.1 ⊢ 𝑅 We 𝐴
wfrlem10OLD.2 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion wfrlem10OLD ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) = dom 𝐹 )

Proof

Step Hyp Ref Expression
1 wfrlem10OLD.1 ⊢ 𝑅 We 𝐴
2 wfrlem10OLD.2 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
3 2 wfrlem8OLD ⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑧 ) = Pred ( 𝑅 , dom 𝐹 , 𝑧 ) )
4 3 biimpi ⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ → Pred ( 𝑅 , 𝐴 , 𝑧 ) = Pred ( 𝑅 , dom 𝐹 , 𝑧 ) )
5 predss ⊢ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ⊆ dom 𝐹
6 5 a1i ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ⊆ dom 𝐹 )
7 simpr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → 𝑤 ∈ dom 𝐹 )
8 eldifn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
9 eleq1w ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ dom 𝐹 ↔ 𝑧 ∈ dom 𝐹 ) )
10 9 notbid ⊢ ( 𝑤 = 𝑧 → ( ¬ 𝑤 ∈ dom 𝐹 ↔ ¬ 𝑧 ∈ dom 𝐹 ) )
11 8 10 syl5ibrcom ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( 𝑤 = 𝑧 → ¬ 𝑤 ∈ dom 𝐹 ) )
12 11 con2d ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( 𝑤 ∈ dom 𝐹 → ¬ 𝑤 = 𝑧 ) )
13 12 imp ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → ¬ 𝑤 = 𝑧 )
14 ssel ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) → 𝑧 ∈ dom 𝐹 ) )
15 14 con3d ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 → ( ¬ 𝑧 ∈ dom 𝐹 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
16 8 15 syl5com ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
17 2 wfrdmclOLD ⊢ ( 𝑤 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
18 16 17 impel ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) )
19 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝑧 ∈ 𝐴 )
20 elpredg ⊢ ( ( 𝑤 ∈ dom 𝐹 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) ↔ 𝑧 𝑅 𝑤 ) )
21 20 ancoms ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ dom 𝐹 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) ↔ 𝑧 𝑅 𝑤 ) )
22 19 21 sylan ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) ↔ 𝑧 𝑅 𝑤 ) )
23 18 22 mtbid ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → ¬ 𝑧 𝑅 𝑤 )
24 2 wfrdmssOLD ⊢ dom 𝐹 ⊆ 𝐴
25 24 sseli ⊢ ( 𝑤 ∈ dom 𝐹 → 𝑤 ∈ 𝐴 )
26 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
27 1 26 ax-mp ⊢ 𝑅 Or 𝐴
28 solin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
29 27 28 mpan ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
30 25 19 29 syl2anr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
31 13 23 30 ecase23d ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → 𝑤 𝑅 𝑧 )
32 vex ⊢ 𝑤 ∈ V
33 32 elpred ⊢ ( 𝑧 ∈ V → ( 𝑤 ∈ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ↔ ( 𝑤 ∈ dom 𝐹 ∧ 𝑤 𝑅 𝑧 ) ) )
34 33 elv ⊢ ( 𝑤 ∈ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ↔ ( 𝑤 ∈ dom 𝐹 ∧ 𝑤 𝑅 𝑧 ) )
35 7 31 34 sylanbrc ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ dom 𝐹 ) → 𝑤 ∈ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) )
36 6 35 eqelssd ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → Pred ( 𝑅 , dom 𝐹 , 𝑧 ) = dom 𝐹 )
37 4 36 sylan9eqr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) = dom 𝐹 )