Theorem ordtypecbv

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
	ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
	ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
Assertion	ordtypecbv	⊢ recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = 𝐹

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
2		ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
3		ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4		breq1	⊢ ( 𝑢 = 𝑟 → ( 𝑢 𝑅 𝑣 ↔ 𝑟 𝑅 𝑣 ) )
5	4	notbid	⊢ ( 𝑢 = 𝑟 → ( ¬ 𝑢 𝑅 𝑣 ↔ ¬ 𝑟 𝑅 𝑣 ) )
6	5	cbvralvw	⊢ ( ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑣 )
7		breq2	⊢ ( 𝑣 = 𝑠 → ( 𝑟 𝑅 𝑣 ↔ 𝑟 𝑅 𝑠 ) )
8	7	notbid	⊢ ( 𝑣 = 𝑠 → ( ¬ 𝑟 𝑅 𝑣 ↔ ¬ 𝑟 𝑅 𝑠 ) )
9	8	ralbidv	⊢ ( 𝑣 = 𝑠 → ( ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑣 ↔ ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑠 ) )
10	6 9	syl5bb	⊢ ( 𝑣 = 𝑠 → ( ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑠 ) )
11	10	cbvriotavw	⊢ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) = ( ℩ 𝑠 ∈ 𝐶 ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑠 )
12		breq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 𝑅 𝑤 ↔ 𝑖 𝑅 𝑤 ) )
13	12	cbvralvw	⊢ ( ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑤 )
14		breq2	⊢ ( 𝑤 = 𝑦 → ( 𝑖 𝑅 𝑤 ↔ 𝑖 𝑅 𝑦 ) )
15	14	ralbidv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 ) )
16	13 15	syl5bb	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 ↔ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 ) )
17	16	cbvrabv	⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 } = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 }
18	2 17	eqtri	⊢ 𝐶 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 }
19		rneq	⊢ ( ℎ = 𝑓 → ran ℎ = ran 𝑓 )
20	19	raleqdv	⊢ ( ℎ = 𝑓 → ( ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 ↔ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 ) )
21	20	rabbidv	⊢ ( ℎ = 𝑓 → { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran ℎ 𝑖 𝑅 𝑦 } = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } )
22	18 21	syl5eq	⊢ ( ℎ = 𝑓 → 𝐶 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } )
23	22	raleqdv	⊢ ( ℎ = 𝑓 → ( ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑠 ↔ ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
24	22 23	riotaeqbidv	⊢ ( ℎ = 𝑓 → ( ℩ 𝑠 ∈ 𝐶 ∀ 𝑟 ∈ 𝐶 ¬ 𝑟 𝑅 𝑠 ) = ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
25	11 24	syl5eq	⊢ ( ℎ = 𝑓 → ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) = ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
26	25	cbvmptv	⊢ ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) ) = ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
27	3 26	eqtri	⊢ 𝐺 = ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) )
28		recseq	⊢ ( 𝐺 = ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) → recs ( 𝐺 ) = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) )
29	27 28	ax-mp	⊢ recs ( 𝐺 ) = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) )
30	1 29	eqtr2i	⊢ recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑠 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = 𝐹