Theorem wfrlem16

Description: Lemma for well-founded recursion. If z is R minimal in ( A \ dom F ) , then C is acceptable and thus a subset of F , but dom C is bigger than dom F . Thus, z cannot be minimal, so ( A \ dom F ) must be empty, and (due to wfrdmss ), dom F = A . (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypotheses	wfrlem13.1	⊢ 𝑅 We 𝐴
	wfrlem13.2	⊢ 𝑅 Se 𝐴
	wfrlem13.3	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
	wfrlem13.4	⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
Assertion	wfrlem16	⊢ dom 𝐹 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		wfrlem13.1	⊢ 𝑅 We 𝐴
2		wfrlem13.2	⊢ 𝑅 Se 𝐴
3		wfrlem13.3	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4		wfrlem13.4	⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5	3	wfrdmss	⊢ dom 𝐹 ⊆ 𝐴
6		eldifn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
7		ssun2	⊢ { 𝑧 } ⊆ ( dom 𝐹 ∪ { 𝑧 } )
8		vsnid	⊢ 𝑧 ∈ { 𝑧 }
9	7 8	sselii	⊢ 𝑧 ∈ ( dom 𝐹 ∪ { 𝑧 } )
10	4	dmeqi	⊢ dom 𝐶 = dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
11		dmun	⊢ dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
12		fvex	⊢ ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
13	12	dmsnop	⊢ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } = { 𝑧 }
14	13	uneq2i	⊢ ( dom 𝐹 ∪ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ { 𝑧 } )
15	10 11 14	3eqtri	⊢ dom 𝐶 = ( dom 𝐹 ∪ { 𝑧 } )
16	9 15	eleqtrri	⊢ 𝑧 ∈ dom 𝐶
17	1 2 3 4	wfrlem15	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
18		elssuni	⊢ ( 𝐶 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝐶 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
19	17 18	syl	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
20		df-wrecs	⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
21	3 20	eqtri	⊢ 𝐹 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
22	19 21	sseqtrrdi	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ⊆ 𝐹 )
23		dmss	⊢ ( 𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹 )
24	22 23	syl	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → dom 𝐶 ⊆ dom 𝐹 )
25	24	sseld	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( 𝑧 ∈ dom 𝐶 → 𝑧 ∈ dom 𝐹 ) )
26	16 25	mpi	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝑧 ∈ dom 𝐹 )
27	6 26	mtand	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
28	27	nrex	⊢ ¬ ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅
29		df-ne	⊢ ( ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ )
30		difss	⊢ ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴
31	1 2	tz6.26i	⊢ ( ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
32	30 31	mpan	⊢ ( ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
33	29 32	sylbir	⊢ ( ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
34	28 33	mt3	⊢ ( 𝐴 ∖ dom 𝐹 ) = ∅
35		ssdif0	⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ( 𝐴 ∖ dom 𝐹 ) = ∅ )
36	34 35	mpbir	⊢ 𝐴 ⊆ dom 𝐹
37	5 36	eqssi	⊢ dom 𝐹 = 𝐴