Theorem wfrlem10

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 . (Contributed by Scott Fenton, 21-Apr-2011)

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

Proof

Step	Hyp	Ref	Expression
1		wfrlem10.1	⊢ 𝑅 We 𝐴
2		wfrlem10.2	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
3	2	wfrlem8	⊢ ( 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	wfrdmcl	⊢ ( 𝑤 ∈ 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	wfrdmss	⊢ 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 𝐹 )