Theorem aomclem2

Description: Lemma for dfac11 . Successor case 2, a choice function for subsets of ( R1dom z ) . (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	aomclem2.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
	aomclem2.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
	aomclem2.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
	aomclem2.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
	aomclem2.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
	aomclem2.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	aomclem2.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
	aomclem2.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion	aomclem2	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem2.b	⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2		aomclem2.c	⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3		aomclem2.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
4		aomclem2.su	⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
5		aomclem2.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
6		aomclem2.a	⊢ ( 𝜑 → 𝐴 ∈ On )
7		aomclem2.za	⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
8		aomclem2.y	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
9		vex	⊢ 𝑎 ∈ V
10	3 6	jca	⊢ ( 𝜑 → ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) )
11		r1ord3	⊢ ( ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) → ( dom 𝑧 ⊆ 𝐴 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
12	10 7 11	sylc	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
13	12	sspwd	⊢ ( 𝜑 → 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝐴 ) )
14	13	sseld	⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) )
15		rsp	⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) )
16	8 14 15	sylsyld	⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) )
17	16	3imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) )
18	17	eldifad	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) )
19		inss1	⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑎
20	19	sseli	⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ∈ 𝒫 𝑎 )
21	20	elpwid	⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 )
22	18 21	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 )
23	1 3 4 5	aomclem1	⊢ ( 𝜑 → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )
24	23	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )
25		inss2	⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ Fin
26	25 18	sselid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ Fin )
27		eldifsni	⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ )
28	17 27	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ )
29		elpwi	⊢ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
30	29	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
31	22 30	sstrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
32		fisupcl	⊢ ( ( 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ∧ ( ( 𝑦 ‘ 𝑎 ) ∈ Fin ∧ ( 𝑦 ‘ 𝑎 ) ≠ ∅ ∧ ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) )
33	24 26 28 31 32	syl13anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) )
34	22 33	sseldd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 )
35	2	fvmpt2	⊢ ( ( 𝑎 ∈ V ∧ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
36	9 34 35	sylancr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
37	36 34	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 )
38	37	3exp	⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ) )
39	38	ralrimiv	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )