Theorem zorn2lem2

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	zorn2lem2	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2		zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3		zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4	1 2 3	zorn2lem1	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
5		breq2	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑔 𝑅 𝑧 ↔ 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
6	5	ralbidv	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
7	6 3	elrab2	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ∧ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
8	7	simprbi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 → ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) )
9	4 8	syl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) )
10	1	tfr1	⊢ 𝐹 Fn On
11		onss	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
12		fnfvima	⊢ ( ( 𝐹 Fn On ∧ 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) )
13	12	3expia	⊢ ( ( 𝐹 Fn On ∧ 𝑥 ⊆ On ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
14	10 11 13	sylancr	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
15	14	adantr	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
16		breq1	⊢ ( 𝑔 = ( 𝐹 ‘ 𝑦 ) → ( 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
17	16	rspccv	⊢ ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
18	9 15 17	sylsyld	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )