Theorem zorn2lem4

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	zorn2lem4	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ∃ 𝑥 ∈ On 𝐷 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2		zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3		zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4		pm3.24	⊢ ¬ ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V )
5		df-ne	⊢ ( 𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅ )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀ 𝑥 ∈ On ¬ 𝐷 = ∅ )
7		df-ral	⊢ ( ∀ 𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) )
8		ralnex	⊢ ( ∀ 𝑥 ∈ On ¬ 𝐷 = ∅ ↔ ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ )
9	6 7 8	3bitr3i	⊢ ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ↔ ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ )
10		weso	⊢ ( 𝑤 We 𝐴 → 𝑤 Or 𝐴 )
11	10	adantr	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → 𝑤 Or 𝐴 )
12		vex	⊢ 𝑤 ∈ V
13		soex	⊢ ( ( 𝑤 Or 𝐴 ∧ 𝑤 ∈ V ) → 𝐴 ∈ V )
14	11 12 13	sylancl	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → 𝐴 ∈ V )
15	1	tfr1	⊢ 𝐹 Fn On
16		fvelrnb	⊢ ( 𝐹 Fn On → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
17	15 16	ax-mp	⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 )
18		nfv	⊢ Ⅎ 𝑥 𝑤 We 𝐴
19		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ )
20	18 19	nfan	⊢ Ⅎ 𝑥 ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) )
21		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
22	3	ssrab3	⊢ 𝐷 ⊆ 𝐴
23	1 2 3	zorn2lem1	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
24	22 23	sselid	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
25		eleq1	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
26	24 25	syl5ibcom	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) )
27	26	exp32	⊢ ( 𝑥 ∈ On → ( 𝑤 We 𝐴 → ( 𝐷 ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
28	27	com12	⊢ ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
29	28	a2d	⊢ ( 𝑤 We 𝐴 → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
30	29	spsd	⊢ ( 𝑤 We 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
31	30	imp	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) )
32	20 21 31	rexlimd	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) )
33	17 32	syl5bi	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐴 ) )
34	33	ssrdv	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ran 𝐹 ⊆ 𝐴 )
35	14 34	ssexd	⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ran 𝐹 ∈ V )
36	35	ex	⊢ ( 𝑤 We 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ran 𝐹 ∈ V ) )
37	36	adantl	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ran 𝐹 ∈ V ) )
38	1 2 3	zorn2lem3	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
39	38	exp45	⊢ ( 𝑅 Po 𝐴 → ( 𝑥 ∈ On → ( 𝑤 We 𝐴 → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
40	39	com23	⊢ ( 𝑅 Po 𝐴 → ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
41	40	imp	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
42	41	a2d	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
43	42	imp4a	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
44	43	alrimdv	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
45	44	alimdv	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
46		r2al	⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
47	45 46	syl6ibr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
48		ssid	⊢ On ⊆ On
49	15	tz7.48lem	⊢ ( ( On ⊆ On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ On ) )
50	48 49	mpan	⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → Fun ◡ ( 𝐹 ↾ On ) )
51		fnrel	⊢ ( 𝐹 Fn On → Rel 𝐹 )
52	15 51	ax-mp	⊢ Rel 𝐹
53	15	fndmi	⊢ dom 𝐹 = On
54	53	eqimssi	⊢ dom 𝐹 ⊆ On
55		relssres	⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ On ) → ( 𝐹 ↾ On ) = 𝐹 )
56	52 54 55	mp2an	⊢ ( 𝐹 ↾ On ) = 𝐹
57	56	cnveqi	⊢ ◡ ( 𝐹 ↾ On ) = ◡ 𝐹
58	57	funeqi	⊢ ( Fun ◡ ( 𝐹 ↾ On ) ↔ Fun ◡ 𝐹 )
59	50 58	sylib	⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → Fun ◡ 𝐹 )
60	47 59	syl6	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → Fun ◡ 𝐹 ) )
61		onprc	⊢ ¬ On ∈ V
62		funrnex	⊢ ( dom ◡ 𝐹 ∈ V → ( Fun ◡ 𝐹 → ran ◡ 𝐹 ∈ V ) )
63	62	com12	⊢ ( Fun ◡ 𝐹 → ( dom ◡ 𝐹 ∈ V → ran ◡ 𝐹 ∈ V ) )
64		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
65	64	eleq1i	⊢ ( ran 𝐹 ∈ V ↔ dom ◡ 𝐹 ∈ V )
66		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
67	53 66	eqtr3i	⊢ On = ran ◡ 𝐹
68	67	eleq1i	⊢ ( On ∈ V ↔ ran ◡ 𝐹 ∈ V )
69	63 65 68	3imtr4g	⊢ ( Fun ◡ 𝐹 → ( ran 𝐹 ∈ V → On ∈ V ) )
70	61 69	mtoi	⊢ ( Fun ◡ 𝐹 → ¬ ran 𝐹 ∈ V )
71	60 70	syl6	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ¬ ran 𝐹 ∈ V ) )
72	37 71	jcad	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V ) ) )
73	9 72	syl5bir	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ → ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V ) ) )
74	4 73	mt3i	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ∃ 𝑥 ∈ On 𝐷 = ∅ )