poseq

Description: A partial ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011)

	Ref	Expression
Hypotheses	poseq.1	$⊢ R Po (A \cup \{\emptyset\})$
	poseq.2	$⊢ F = \{f \| \exists x \in On f : x ⟶ A\}$
	poseq.3	$⊢ S = \{⟨f, g⟩ \| ((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)))\}$
Assertion	poseq	$⊢ S Po F$

Proof

Step	Hyp	Ref	Expression
1		poseq.1	$⊢ R Po (A \cup \{\emptyset\})$
2		poseq.2	$⊢ F = \{f \| \exists x \in On f : x ⟶ A\}$
3		poseq.3	$⊢ S = \{⟨f, g⟩ \| ((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)))\}$
4		feq2	$⊢ x = b \to (f : x ⟶ A \leftrightarrow f : b ⟶ A)$
5	4	cbvrexvw	$⊢ \exists x \in On f : x ⟶ A \leftrightarrow \exists b \in On f : b ⟶ A$
6	5	abbii	$⊢ \{f \| \exists x \in On f : x ⟶ A\} = \{f \| \exists b \in On f : b ⟶ A\}$
7	2 6	eqtri	$⊢ F = \{f \| \exists b \in On f : b ⟶ A\}$
8	7	orderseqlem	$⊢ a \in F \to a (x) \in (A \cup \{\emptyset\})$
9		poirr	$⊢ (R Po (A \cup \{\emptyset\}) \land a (x) \in (A \cup \{\emptyset\})) \to \neg a (x) R a (x)$
10	1 8 9	sylancr	$⊢ a \in F \to \neg a (x) R a (x)$
11	10	intnand	$⊢ a \in F \to \neg (\forall y \in x a (y) = a (y) \land a (x) R a (x))$
12	11	adantr	$⊢ (a \in F \land x \in On) \to \neg (\forall y \in x a (y) = a (y) \land a (x) R a (x))$
13	12	nrexdv	$⊢ a \in F \to \neg \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x))$
14	13	adantr	$⊢ (a \in F \land a \in F) \to \neg \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x))$
15		imnan	$⊢ ((a \in F \land a \in F) \to \neg \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x))) \leftrightarrow \neg ((a \in F \land a \in F) \land \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x)))$
16	14 15	mpbi	$⊢ \neg ((a \in F \land a \in F) \land \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x)))$
17		vex	$⊢ a \in V$
18		eleq1w	$⊢ f = a \to (f \in F \leftrightarrow a \in F)$
19	18	anbi1d	$⊢ f = a \to ((f \in F \land g \in F) \leftrightarrow (a \in F \land g \in F))$
20		fveq1	$⊢ f = a \to f (y) = a (y)$
21	20	eqeq1d	$⊢ f = a \to (f (y) = g (y) \leftrightarrow a (y) = g (y))$
22	21	ralbidv	$⊢ f = a \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in x a (y) = g (y))$
23		fveq1	$⊢ f = a \to f (x) = a (x)$
24	23	breq1d	$⊢ f = a \to (f (x) R g (x) \leftrightarrow a (x) R g (x))$
25	22 24	anbi12d	$⊢ f = a \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in x a (y) = g (y) \land a (x) R g (x)))$
26	25	rexbidv	$⊢ f = a \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x)))$
27	19 26	anbi12d	$⊢ f = a \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((a \in F \land g \in F) \land \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x))))$
28		eleq1w	$⊢ g = a \to (g \in F \leftrightarrow a \in F)$
29	28	anbi2d	$⊢ g = a \to ((a \in F \land g \in F) \leftrightarrow (a \in F \land a \in F))$
30		fveq1	$⊢ g = a \to g (y) = a (y)$
31	30	eqeq2d	$⊢ g = a \to (a (y) = g (y) \leftrightarrow a (y) = a (y))$
32	31	ralbidv	$⊢ g = a \to (\forall y \in x a (y) = g (y) \leftrightarrow \forall y \in x a (y) = a (y))$
33		fveq1	$⊢ g = a \to g (x) = a (x)$
34	33	breq2d	$⊢ g = a \to (a (x) R g (x) \leftrightarrow a (x) R a (x))$
35	32 34	anbi12d	$⊢ g = a \to ((\forall y \in x a (y) = g (y) \land a (x) R g (x)) \leftrightarrow (\forall y \in x a (y) = a (y) \land a (x) R a (x)))$
36	35	rexbidv	$⊢ g = a \to (\exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x)))$
37	29 36	anbi12d	$⊢ g = a \to (((a \in F \land g \in F) \land \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x))) \leftrightarrow ((a \in F \land a \in F) \land \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x))))$
38	17 17 27 37 3	brab	$⊢ a S a \leftrightarrow ((a \in F \land a \in F) \land \exists x \in On (\forall y \in x a (y) = a (y) \land a (x) R a (x)))$
39	16 38	mtbir	$⊢ \neg a S a$
40		vex	$⊢ b \in V$
41		raleq	$⊢ x = z \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in z f (y) = g (y))$
42		fveq2	$⊢ x = z \to f (x) = f (z)$
43		fveq2	$⊢ x = z \to g (x) = g (z)$
44	42 43	breq12d	$⊢ x = z \to (f (x) R g (x) \leftrightarrow f (z) R g (z))$
45	41 44	anbi12d	$⊢ x = z \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in z f (y) = g (y) \land f (z) R g (z)))$
46	45	cbvrexvw	$⊢ \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists z \in On (\forall y \in z f (y) = g (y) \land f (z) R g (z))$
47	21	ralbidv	$⊢ f = a \to (\forall y \in z f (y) = g (y) \leftrightarrow \forall y \in z a (y) = g (y))$
48		fveq1	$⊢ f = a \to f (z) = a (z)$
49	48	breq1d	$⊢ f = a \to (f (z) R g (z) \leftrightarrow a (z) R g (z))$
50	47 49	anbi12d	$⊢ f = a \to ((\forall y \in z f (y) = g (y) \land f (z) R g (z)) \leftrightarrow (\forall y \in z a (y) = g (y) \land a (z) R g (z)))$
51	50	rexbidv	$⊢ f = a \to (\exists z \in On (\forall y \in z f (y) = g (y) \land f (z) R g (z)) \leftrightarrow \exists z \in On (\forall y \in z a (y) = g (y) \land a (z) R g (z)))$
52	46 51	bitrid	$⊢ f = a \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists z \in On (\forall y \in z a (y) = g (y) \land a (z) R g (z)))$
53	19 52	anbi12d	$⊢ f = a \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((a \in F \land g \in F) \land \exists z \in On (\forall y \in z a (y) = g (y) \land a (z) R g (z))))$
54		eleq1w	$⊢ g = b \to (g \in F \leftrightarrow b \in F)$
55	54	anbi2d	$⊢ g = b \to ((a \in F \land g \in F) \leftrightarrow (a \in F \land b \in F))$
56		fveq1	$⊢ g = b \to g (y) = b (y)$
57	56	eqeq2d	$⊢ g = b \to (a (y) = g (y) \leftrightarrow a (y) = b (y))$
58	57	ralbidv	$⊢ g = b \to (\forall y \in z a (y) = g (y) \leftrightarrow \forall y \in z a (y) = b (y))$
59		fveq1	$⊢ g = b \to g (z) = b (z)$
60	59	breq2d	$⊢ g = b \to (a (z) R g (z) \leftrightarrow a (z) R b (z))$
61	58 60	anbi12d	$⊢ g = b \to ((\forall y \in z a (y) = g (y) \land a (z) R g (z)) \leftrightarrow (\forall y \in z a (y) = b (y) \land a (z) R b (z)))$
62	61	rexbidv	$⊢ g = b \to (\exists z \in On (\forall y \in z a (y) = g (y) \land a (z) R g (z)) \leftrightarrow \exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)))$
63	55 62	anbi12d	$⊢ g = b \to (((a \in F \land g \in F) \land \exists z \in On (\forall y \in z a (y) = g (y) \land a (z) R g (z))) \leftrightarrow ((a \in F \land b \in F) \land \exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z))))$
64	17 40 53 63 3	brab	$⊢ a S b \leftrightarrow ((a \in F \land b \in F) \land \exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)))$
65		vex	$⊢ c \in V$
66		eleq1w	$⊢ f = b \to (f \in F \leftrightarrow b \in F)$
67	66	anbi1d	$⊢ f = b \to ((f \in F \land g \in F) \leftrightarrow (b \in F \land g \in F))$
68		raleq	$⊢ x = w \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in w f (y) = g (y))$
69		fveq2	$⊢ x = w \to f (x) = f (w)$
70		fveq2	$⊢ x = w \to g (x) = g (w)$
71	69 70	breq12d	$⊢ x = w \to (f (x) R g (x) \leftrightarrow f (w) R g (w))$
72	68 71	anbi12d	$⊢ x = w \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in w f (y) = g (y) \land f (w) R g (w)))$
73	72	cbvrexvw	$⊢ \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists w \in On (\forall y \in w f (y) = g (y) \land f (w) R g (w))$
74		fveq1	$⊢ f = b \to f (y) = b (y)$
75	74	eqeq1d	$⊢ f = b \to (f (y) = g (y) \leftrightarrow b (y) = g (y))$
76	75	ralbidv	$⊢ f = b \to (\forall y \in w f (y) = g (y) \leftrightarrow \forall y \in w b (y) = g (y))$
77		fveq1	$⊢ f = b \to f (w) = b (w)$
78	77	breq1d	$⊢ f = b \to (f (w) R g (w) \leftrightarrow b (w) R g (w))$
79	76 78	anbi12d	$⊢ f = b \to ((\forall y \in w f (y) = g (y) \land f (w) R g (w)) \leftrightarrow (\forall y \in w b (y) = g (y) \land b (w) R g (w)))$
80	79	rexbidv	$⊢ f = b \to (\exists w \in On (\forall y \in w f (y) = g (y) \land f (w) R g (w)) \leftrightarrow \exists w \in On (\forall y \in w b (y) = g (y) \land b (w) R g (w)))$
81	73 80	bitrid	$⊢ f = b \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists w \in On (\forall y \in w b (y) = g (y) \land b (w) R g (w)))$
82	67 81	anbi12d	$⊢ f = b \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((b \in F \land g \in F) \land \exists w \in On (\forall y \in w b (y) = g (y) \land b (w) R g (w))))$
83		eleq1w	$⊢ g = c \to (g \in F \leftrightarrow c \in F)$
84	83	anbi2d	$⊢ g = c \to ((b \in F \land g \in F) \leftrightarrow (b \in F \land c \in F))$
85		fveq1	$⊢ g = c \to g (y) = c (y)$
86	85	eqeq2d	$⊢ g = c \to (b (y) = g (y) \leftrightarrow b (y) = c (y))$
87	86	ralbidv	$⊢ g = c \to (\forall y \in w b (y) = g (y) \leftrightarrow \forall y \in w b (y) = c (y))$
88		fveq1	$⊢ g = c \to g (w) = c (w)$
89	88	breq2d	$⊢ g = c \to (b (w) R g (w) \leftrightarrow b (w) R c (w))$
90	87 89	anbi12d	$⊢ g = c \to ((\forall y \in w b (y) = g (y) \land b (w) R g (w)) \leftrightarrow (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
91	90	rexbidv	$⊢ g = c \to (\exists w \in On (\forall y \in w b (y) = g (y) \land b (w) R g (w)) \leftrightarrow \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
92	84 91	anbi12d	$⊢ g = c \to (((b \in F \land g \in F) \land \exists w \in On (\forall y \in w b (y) = g (y) \land b (w) R g (w))) \leftrightarrow ((b \in F \land c \in F) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w))))$
93	40 65 82 92 3	brab	$⊢ b S c \leftrightarrow ((b \in F \land c \in F) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
94		simplll	$⊢ (((a \in F \land b \in F) \land (b \in F \land c \in F)) \land (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))) \to a \in F$
95		simplrr	$⊢ (((a \in F \land b \in F) \land (b \in F \land c \in F)) \land (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))) \to c \in F$
96		an4	$⊢ ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \leftrightarrow ((\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
97	96	2rexbii	$⊢ \exists z \in On \exists w \in On ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \leftrightarrow \exists z \in On \exists w \in On ((\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
98		reeanv	$⊢ \exists z \in On \exists w \in On ((\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land (\forall y \in w b (y) = c (y) \land b (w) R c (w))) \leftrightarrow (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
99	97 98	bitri	$⊢ \exists z \in On \exists w \in On ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \leftrightarrow (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))$
100		eloni	$⊢ z \in On \to Ord z$
101		eloni	$⊢ w \in On \to Ord w$
102		ordtri3or	$⊢ (Ord z \land Ord w) \to (z \in w \lor z = w \lor w \in z)$
103	100 101 102	syl2an	$⊢ (z \in On \land w \in On) \to (z \in w \lor z = w \lor w \in z)$
104		simp1l	$⊢ ((z \in On \land w \in On) \land z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to z \in On$
105		onelss	$⊢ w \in On \to (z \in w \to z \subseteq w)$
106	105	imp	$⊢ (w \in On \land z \in w) \to z \subseteq w$
107	106	adantll	$⊢ ((z \in On \land w \in On) \land z \in w) \to z \subseteq w$
108		ssralv	$⊢ z \subseteq w \to (\forall y \in w b (y) = c (y) \to \forall y \in z b (y) = c (y))$
109	108	anim2d	$⊢ z \subseteq w \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to (\forall y \in z a (y) = b (y) \land \forall y \in z b (y) = c (y)))$
110		r19.26	$⊢ \forall y \in z (a (y) = b (y) \land b (y) = c (y)) \leftrightarrow (\forall y \in z a (y) = b (y) \land \forall y \in z b (y) = c (y))$
111	109 110	imbitrrdi	$⊢ z \subseteq w \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to \forall y \in z (a (y) = b (y) \land b (y) = c (y)))$
112		eqtr	$⊢ (a (y) = b (y) \land b (y) = c (y)) \to a (y) = c (y)$
113	112	ralimi	$⊢ \forall y \in z (a (y) = b (y) \land b (y) = c (y)) \to \forall y \in z a (y) = c (y)$
114	111 113	syl6	$⊢ z \subseteq w \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to \forall y \in z a (y) = c (y))$
115	107 114	syl	$⊢ ((z \in On \land w \in On) \land z \in w) \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to \forall y \in z a (y) = c (y))$
116	115	adantrd	$⊢ ((z \in On \land w \in On) \land z \in w) \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to \forall y \in z a (y) = c (y))$
117	116	3impia	$⊢ ((z \in On \land w \in On) \land z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to \forall y \in z a (y) = c (y)$
118		fveq2	$⊢ y = z \to b (y) = b (z)$
119		fveq2	$⊢ y = z \to c (y) = c (z)$
120	118 119	eqeq12d	$⊢ y = z \to (b (y) = c (y) \leftrightarrow b (z) = c (z))$
121	120	rspcv	$⊢ z \in w \to (\forall y \in w b (y) = c (y) \to b (z) = c (z))$
122		breq2	$⊢ b (z) = c (z) \to (a (z) R b (z) \leftrightarrow a (z) R c (z))$
123	122	biimpd	$⊢ b (z) = c (z) \to (a (z) R b (z) \to a (z) R c (z))$
124	121 123	syl6	$⊢ z \in w \to (\forall y \in w b (y) = c (y) \to (a (z) R b (z) \to a (z) R c (z)))$
125	124	com3l	$⊢ \forall y \in w b (y) = c (y) \to (a (z) R b (z) \to (z \in w \to a (z) R c (z)))$
126	125	imp	$⊢ (\forall y \in w b (y) = c (y) \land a (z) R b (z)) \to (z \in w \to a (z) R c (z))$
127	126	ad2ant2lr	$⊢ ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (z \in w \to a (z) R c (z))$
128	127	impcom	$⊢ (z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to a (z) R c (z)$
129	128	3adant1	$⊢ ((z \in On \land w \in On) \land z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to a (z) R c (z)$
130		raleq	$⊢ t = z \to (\forall y \in t a (y) = c (y) \leftrightarrow \forall y \in z a (y) = c (y))$
131		fveq2	$⊢ t = z \to a (t) = a (z)$
132		fveq2	$⊢ t = z \to c (t) = c (z)$
133	131 132	breq12d	$⊢ t = z \to (a (t) R c (t) \leftrightarrow a (z) R c (z))$
134	130 133	anbi12d	$⊢ t = z \to ((\forall y \in t a (y) = c (y) \land a (t) R c (t)) \leftrightarrow (\forall y \in z a (y) = c (y) \land a (z) R c (z)))$
135	134	rspcev	$⊢ (z \in On \land (\forall y \in z a (y) = c (y) \land a (z) R c (z))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
136	104 117 129 135	syl12anc	$⊢ ((z \in On \land w \in On) \land z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
137	136	a1d	$⊢ ((z \in On \land w \in On) \land z \in w \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
138	137	3exp	$⊢ (z \in On \land w \in On) \to (z \in w \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
139	2	orderseqlem	$⊢ a \in F \to a (z) \in (A \cup \{\emptyset\})$
140	139	ad2antrr	$⊢ ((a \in F \land b \in F) \land (b \in F \land c \in F)) \to a (z) \in (A \cup \{\emptyset\})$
141	2	orderseqlem	$⊢ b \in F \to b (z) \in (A \cup \{\emptyset\})$
142	141	ad2antlr	$⊢ ((a \in F \land b \in F) \land (b \in F \land c \in F)) \to b (z) \in (A \cup \{\emptyset\})$
143	2	orderseqlem	$⊢ c \in F \to c (z) \in (A \cup \{\emptyset\})$
144	143	ad2antll	$⊢ ((a \in F \land b \in F) \land (b \in F \land c \in F)) \to c (z) \in (A \cup \{\emptyset\})$
145	140 142 144	3jca	$⊢ ((a \in F \land b \in F) \land (b \in F \land c \in F)) \to (a (z) \in (A \cup \{\emptyset\}) \land b (z) \in (A \cup \{\emptyset\}) \land c (z) \in (A \cup \{\emptyset\}))$
146		potr	$⊢ (R Po (A \cup \{\emptyset\}) \land (a (z) \in (A \cup \{\emptyset\}) \land b (z) \in (A \cup \{\emptyset\}) \land c (z) \in (A \cup \{\emptyset\}))) \to ((a (z) R b (z) \land b (z) R c (z)) \to a (z) R c (z))$
147	1 145 146	sylancr	$⊢ ((a \in F \land b \in F) \land (b \in F \land c \in F)) \to ((a (z) R b (z) \land b (z) R c (z)) \to a (z) R c (z))$
148	147	impcom	$⊢ ((a (z) R b (z) \land b (z) R c (z)) \land ((a \in F \land b \in F) \land (b \in F \land c \in F))) \to a (z) R c (z)$
149	113 148	anim12i	$⊢ (\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land ((a (z) R b (z) \land b (z) R c (z)) \land ((a \in F \land b \in F) \land (b \in F \land c \in F)))) \to (\forall y \in z a (y) = c (y) \land a (z) R c (z))$
150	149	anassrs	$⊢ ((\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land (a (z) R b (z) \land b (z) R c (z))) \land ((a \in F \land b \in F) \land (b \in F \land c \in F))) \to (\forall y \in z a (y) = c (y) \land a (z) R c (z))$
151	150 135	sylan2	$⊢ (z \in On \land ((\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land (a (z) R b (z) \land b (z) R c (z))) \land ((a \in F \land b \in F) \land (b \in F \land c \in F)))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
152	151	exp32	$⊢ z \in On \to ((\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land (a (z) R b (z) \land b (z) R c (z))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))))$
153		raleq	$⊢ z = w \to (\forall y \in z b (y) = c (y) \leftrightarrow \forall y \in w b (y) = c (y))$
154	153	anbi2d	$⊢ z = w \to ((\forall y \in z a (y) = b (y) \land \forall y \in z b (y) = c (y)) \leftrightarrow (\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)))$
155	110 154	bitrid	$⊢ z = w \to (\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \leftrightarrow (\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)))$
156		fveq2	$⊢ z = w \to b (z) = b (w)$
157		fveq2	$⊢ z = w \to c (z) = c (w)$
158	156 157	breq12d	$⊢ z = w \to (b (z) R c (z) \leftrightarrow b (w) R c (w))$
159	158	anbi2d	$⊢ z = w \to ((a (z) R b (z) \land b (z) R c (z)) \leftrightarrow (a (z) R b (z) \land b (w) R c (w)))$
160	155 159	anbi12d	$⊢ z = w \to ((\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land (a (z) R b (z) \land b (z) R c (z))) \leftrightarrow ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))))$
161	160	imbi1d	$⊢ z = w \to (((\forall y \in z (a (y) = b (y) \land b (y) = c (y)) \land (a (z) R b (z) \land b (z) R c (z))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))) \leftrightarrow (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
162	152 161	syl5ibcom	$⊢ z \in On \to (z = w \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
163	162	adantr	$⊢ (z \in On \land w \in On) \to (z = w \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
164		simp1r	$⊢ ((z \in On \land w \in On) \land w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to w \in On$
165		onelss	$⊢ z \in On \to (w \in z \to w \subseteq z)$
166	165	imp	$⊢ (z \in On \land w \in z) \to w \subseteq z$
167	166	adantlr	$⊢ ((z \in On \land w \in On) \land w \in z) \to w \subseteq z$
168		ssralv	$⊢ w \subseteq z \to (\forall y \in z a (y) = b (y) \to \forall y \in w a (y) = b (y))$
169	168	anim1d	$⊢ w \subseteq z \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to (\forall y \in w a (y) = b (y) \land \forall y \in w b (y) = c (y)))$
170		r19.26	$⊢ \forall y \in w (a (y) = b (y) \land b (y) = c (y)) \leftrightarrow (\forall y \in w a (y) = b (y) \land \forall y \in w b (y) = c (y))$
171	112	ralimi	$⊢ \forall y \in w (a (y) = b (y) \land b (y) = c (y)) \to \forall y \in w a (y) = c (y)$
172	170 171	sylbir	$⊢ (\forall y \in w a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to \forall y \in w a (y) = c (y)$
173	169 172	syl6	$⊢ w \subseteq z \to ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \to \forall y \in w a (y) = c (y))$
174	173	adantrd	$⊢ w \subseteq z \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to \forall y \in w a (y) = c (y))$
175	167 174	syl	$⊢ ((z \in On \land w \in On) \land w \in z) \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to \forall y \in w a (y) = c (y))$
176	175	3impia	$⊢ ((z \in On \land w \in On) \land w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to \forall y \in w a (y) = c (y)$
177		fveq2	$⊢ y = w \to a (y) = a (w)$
178		fveq2	$⊢ y = w \to b (y) = b (w)$
179	177 178	eqeq12d	$⊢ y = w \to (a (y) = b (y) \leftrightarrow a (w) = b (w))$
180	179	rspcv	$⊢ w \in z \to (\forall y \in z a (y) = b (y) \to a (w) = b (w))$
181		breq1	$⊢ a (w) = b (w) \to (a (w) R c (w) \leftrightarrow b (w) R c (w))$
182	181	biimprd	$⊢ a (w) = b (w) \to (b (w) R c (w) \to a (w) R c (w))$
183	180 182	syl6	$⊢ w \in z \to (\forall y \in z a (y) = b (y) \to (b (w) R c (w) \to a (w) R c (w)))$
184	183	com3l	$⊢ \forall y \in z a (y) = b (y) \to (b (w) R c (w) \to (w \in z \to a (w) R c (w)))$
185	184	imp	$⊢ (\forall y \in z a (y) = b (y) \land b (w) R c (w)) \to (w \in z \to a (w) R c (w))$
186	185	ad2ant2rl	$⊢ ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (w \in z \to a (w) R c (w))$
187	186	impcom	$⊢ (w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to a (w) R c (w)$
188	187	3adant1	$⊢ ((z \in On \land w \in On) \land w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to a (w) R c (w)$
189		raleq	$⊢ t = w \to (\forall y \in t a (y) = c (y) \leftrightarrow \forall y \in w a (y) = c (y))$
190		fveq2	$⊢ t = w \to a (t) = a (w)$
191		fveq2	$⊢ t = w \to c (t) = c (w)$
192	190 191	breq12d	$⊢ t = w \to (a (t) R c (t) \leftrightarrow a (w) R c (w))$
193	189 192	anbi12d	$⊢ t = w \to ((\forall y \in t a (y) = c (y) \land a (t) R c (t)) \leftrightarrow (\forall y \in w a (y) = c (y) \land a (w) R c (w)))$
194	193	rspcev	$⊢ (w \in On \land (\forall y \in w a (y) = c (y) \land a (w) R c (w))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
195	164 176 188 194	syl12anc	$⊢ ((z \in On \land w \in On) \land w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
196	195	a1d	$⊢ ((z \in On \land w \in On) \land w \in z \land ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w)))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
197	196	3exp	$⊢ (z \in On \land w \in On) \to (w \in z \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
198	138 163 197	3jaod	$⊢ (z \in On \land w \in On) \to ((z \in w \lor z = w \lor w \in z) \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))))$
199	103 198	mpd	$⊢ (z \in On \land w \in On) \to (((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))))$
200	199	rexlimivv	$⊢ \exists z \in On \exists w \in On ((\forall y \in z a (y) = b (y) \land \forall y \in w b (y) = c (y)) \land (a (z) R b (z) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
201	99 200	sylbir	$⊢ (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w))) \to (((a \in F \land b \in F) \land (b \in F \land c \in F)) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
202	201	impcom	$⊢ (((a \in F \land b \in F) \land (b \in F \land c \in F)) \land (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))) \to \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))$
203	94 95 202	jca31	$⊢ (((a \in F \land b \in F) \land (b \in F \land c \in F)) \land (\exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z)) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))) \to ((a \in F \land c \in F) \land \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
204	203	an4s	$⊢ (((a \in F \land b \in F) \land \exists z \in On (\forall y \in z a (y) = b (y) \land a (z) R b (z))) \land ((b \in F \land c \in F) \land \exists w \in On (\forall y \in w b (y) = c (y) \land b (w) R c (w)))) \to ((a \in F \land c \in F) \land \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
205	64 93 204	syl2anb	$⊢ (a S b \land b S c) \to ((a \in F \land c \in F) \land \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
206		raleq	$⊢ x = t \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in t f (y) = g (y))$
207		fveq2	$⊢ x = t \to f (x) = f (t)$
208		fveq2	$⊢ x = t \to g (x) = g (t)$
209	207 208	breq12d	$⊢ x = t \to (f (x) R g (x) \leftrightarrow f (t) R g (t))$
210	206 209	anbi12d	$⊢ x = t \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in t f (y) = g (y) \land f (t) R g (t)))$
211	210	cbvrexvw	$⊢ \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists t \in On (\forall y \in t f (y) = g (y) \land f (t) R g (t))$
212	21	ralbidv	$⊢ f = a \to (\forall y \in t f (y) = g (y) \leftrightarrow \forall y \in t a (y) = g (y))$
213		fveq1	$⊢ f = a \to f (t) = a (t)$
214	213	breq1d	$⊢ f = a \to (f (t) R g (t) \leftrightarrow a (t) R g (t))$
215	212 214	anbi12d	$⊢ f = a \to ((\forall y \in t f (y) = g (y) \land f (t) R g (t)) \leftrightarrow (\forall y \in t a (y) = g (y) \land a (t) R g (t)))$
216	215	rexbidv	$⊢ f = a \to (\exists t \in On (\forall y \in t f (y) = g (y) \land f (t) R g (t)) \leftrightarrow \exists t \in On (\forall y \in t a (y) = g (y) \land a (t) R g (t)))$
217	211 216	bitrid	$⊢ f = a \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists t \in On (\forall y \in t a (y) = g (y) \land a (t) R g (t)))$
218	19 217	anbi12d	$⊢ f = a \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((a \in F \land g \in F) \land \exists t \in On (\forall y \in t a (y) = g (y) \land a (t) R g (t))))$
219	83	anbi2d	$⊢ g = c \to ((a \in F \land g \in F) \leftrightarrow (a \in F \land c \in F))$
220	85	eqeq2d	$⊢ g = c \to (a (y) = g (y) \leftrightarrow a (y) = c (y))$
221	220	ralbidv	$⊢ g = c \to (\forall y \in t a (y) = g (y) \leftrightarrow \forall y \in t a (y) = c (y))$
222		fveq1	$⊢ g = c \to g (t) = c (t)$
223	222	breq2d	$⊢ g = c \to (a (t) R g (t) \leftrightarrow a (t) R c (t))$
224	221 223	anbi12d	$⊢ g = c \to ((\forall y \in t a (y) = g (y) \land a (t) R g (t)) \leftrightarrow (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
225	224	rexbidv	$⊢ g = c \to (\exists t \in On (\forall y \in t a (y) = g (y) \land a (t) R g (t)) \leftrightarrow \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
226	219 225	anbi12d	$⊢ g = c \to (((a \in F \land g \in F) \land \exists t \in On (\forall y \in t a (y) = g (y) \land a (t) R g (t))) \leftrightarrow ((a \in F \land c \in F) \land \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t))))$
227	17 65 218 226 3	brab	$⊢ a S c \leftrightarrow ((a \in F \land c \in F) \land \exists t \in On (\forall y \in t a (y) = c (y) \land a (t) R c (t)))$
228	205 227	sylibr	$⊢ (a S b \land b S c) \to a S c$
229	39 228	pm3.2i	$⊢ (\neg a S a \land ((a S b \land b S c) \to a S c))$
230	229	a1i	$⊢ (a \in F \land b \in F \land c \in F) \to (\neg a S a \land ((a S b \land b S c) \to a S c))$
231	230	rgen3	$⊢ \forall a \in F \forall b \in F \forall c \in F (\neg a S a \land ((a S b \land b S c) \to a S c))$
232		df-po	$⊢ S Po F \leftrightarrow \forall a \in F \forall b \in F \forall c \in F (\neg a S a \land ((a S b \land b S c) \to a S c))$
233	231 232	mpbir	$⊢ S Po F$

Metamath Proof Explorer

Theorem poseq

Proof