Theorem zorn2lem1

Description: Lemma for zorn2 . (Contributed by NM, 3-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
	zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
	zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
Assertion	zorn2lem1	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2		zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3		zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4	1	tfr2	⊢ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) )
5	4	adantr	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) )
6	1	tfr1	⊢ 𝐹 Fn On
7		fnfun	⊢ ( 𝐹 Fn On → Fun 𝐹 )
8	6 7	ax-mp	⊢ Fun 𝐹
9		vex	⊢ 𝑥 ∈ V
10		resfunexg	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ V ) → ( 𝐹 ↾ 𝑥 ) ∈ V )
11	8 9 10	mp2an	⊢ ( 𝐹 ↾ 𝑥 ) ∈ V
12		rneq	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ran 𝑓 = ran ( 𝐹 ↾ 𝑥 ) )
13		df-ima	⊢ ( 𝐹 “ 𝑥 ) = ran ( 𝐹 ↾ 𝑥 )
14	12 13	syl6eqr	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ran 𝑓 = ( 𝐹 “ 𝑥 ) )
15	14	eleq2d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝑔 ∈ ran 𝑓 ↔ 𝑔 ∈ ( 𝐹 “ 𝑥 ) ) )
16	15	imbi1d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ( 𝑔 ∈ ran 𝑓 → 𝑔 𝑅 𝑧 ) ↔ ( 𝑔 ∈ ( 𝐹 “ 𝑥 ) → 𝑔 𝑅 𝑧 ) ) )
17	16	ralbidv2	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 ) )
18	17	rabbidv	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 } = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } )
19	18 2 3	3eqtr4g	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → 𝐶 = 𝐷 )
20	19	eleq2d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝑢 ∈ 𝐶 ↔ 𝑢 ∈ 𝐷 ) )
21	20	imbi1d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ( 𝑢 ∈ 𝐶 → ¬ 𝑢 𝑤 𝑣 ) ↔ ( 𝑢 ∈ 𝐷 → ¬ 𝑢 𝑤 𝑣 ) ) )
22	21	ralbidv2	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ↔ ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) )
23	19 22	riotaeqbidv	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) = ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) )
24		eqid	⊢ ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) = ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) )
25		riotaex	⊢ ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ V
26	23 24 25	fvmpt	⊢ ( ( 𝐹 ↾ 𝑥 ) ∈ V → ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) )
27	11 26	ax-mp	⊢ ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 )
28	5 27	syl6eq	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) )
29		simprl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝑤 We 𝐴 )
30		weso	⊢ ( 𝑤 We 𝐴 → 𝑤 Or 𝐴 )
31	30	ad2antrl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝑤 Or 𝐴 )
32		vex	⊢ 𝑤 ∈ V
33		soex	⊢ ( ( 𝑤 Or 𝐴 ∧ 𝑤 ∈ V ) → 𝐴 ∈ V )
34	31 32 33	sylancl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝐴 ∈ V )
35	3 34	rabexd	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝐷 ∈ V )
36	3	ssrab3	⊢ 𝐷 ⊆ 𝐴
37	36	a1i	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝐷 ⊆ 𝐴 )
38		simprr	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → 𝐷 ≠ ∅ )
39		wereu	⊢ ( ( 𝑤 We 𝐴 ∧ ( 𝐷 ∈ V ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ∃! 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 )
40	29 35 37 38 39	syl13anc	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ∃! 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 )
41		riotacl	⊢ ( ∃! 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 → ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ 𝐷 )
42	40 41	syl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( ℩ 𝑣 ∈ 𝐷 ∀ 𝑢 ∈ 𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ 𝐷 )
43	28 42	eqeltrd	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )