Theorem wfrlem8

Description: Lemma for well-founded recursion. Compute the prececessor class for an R minimal element of ( A \ dom F ) . (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypothesis	wfrlem6.1	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	wfrlem8	⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑋 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , dom 𝐹 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
2	1	wfrdmss	⊢ dom 𝐹 ⊆ 𝐴
3		predpredss	⊢ ( dom 𝐹 ⊆ 𝐴 → Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
4	2 3	ax-mp	⊢ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 )
5	4	biantru	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ∧ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
6		preddif	⊢ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) )
7	6	eqeq1i	⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑋 ) = ∅ ↔ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ) = ∅ )
8		ssdif0	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ) = ∅ )
9	7 8	bitr4i	⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑋 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) )
10		eqss	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ∧ Pred ( 𝑅 , dom 𝐹 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
11	5 9 10	3bitr4i	⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑋 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , dom 𝐹 , 𝑋 ) )