Theorem zorn2lem5

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

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

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2		zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3		zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4		zorn2lem.7	⊢ 𝐻 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 }
5	1	tfr1	⊢ 𝐹 Fn On
6		fnfun	⊢ ( 𝐹 Fn On → Fun 𝐹 )
7	5 6	ax-mp	⊢ Fun 𝐹
8		fvelima	⊢ ( ( Fun 𝐹 ∧ 𝑠 ∈ ( 𝐹 “ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 )
9	7 8	mpan	⊢ ( 𝑠 ∈ ( 𝐹 “ 𝑥 ) → ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 )
10		nfv	⊢ Ⅎ 𝑦 ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On )
11		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅
12	10 11	nfan	⊢ Ⅎ 𝑦 ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ )
13		nfv	⊢ Ⅎ 𝑦 𝑠 ∈ 𝐴
14		df-ral	⊢ ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) )
15		onelon	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
16	4	ssrab3	⊢ 𝐻 ⊆ 𝐴
17	1 2 4	zorn2lem1	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐻 )
18	16 17	sselid	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
19		eleq1	⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 ↔ 𝑠 ∈ 𝐴 ) )
20	18 19	syl5ib	⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → 𝑠 ∈ 𝐴 ) )
21	15 20	sylani	⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → 𝑠 ∈ 𝐴 ) )
22	21	com12	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) )
23	22	exp43	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝑤 We 𝐴 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) ) )
24	23	com3r	⊢ ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) ) )
25	24	imp	⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ 𝑥 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
26	25	a2d	⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
27	26	spsd	⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
28	14 27	syl5bi	⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
29	28	imp	⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) )
30	12 13 29	rexlimd	⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) )
31	9 30	syl5	⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝑠 ∈ ( 𝐹 “ 𝑥 ) → 𝑠 ∈ 𝐴 ) )
32	31	ssrdv	⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )