tz7.49

Description: Proposition 7.49 of TakeutiZaring p. 51. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 10-Jan-2013)

	Ref	Expression
Hypotheses	tz7.49.1	$⊢ F Fn On$
	tz7.49.2	$⊢ φ \leftrightarrow \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
Assertion	tz7.49	$⊢ (A \in B \land φ) \to \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		tz7.49.1	$⊢ F Fn On$
2		tz7.49.2	$⊢ φ \leftrightarrow \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
3		df-ne	$⊢ A ∖ F [x] \neq \emptyset \leftrightarrow \neg A ∖ F [x] = \emptyset$
4	3	ralbii	$⊢ \forall x \in On A ∖ F [x] \neq \emptyset \leftrightarrow \forall x \in On \neg A ∖ F [x] = \emptyset$
5		ralim	$⊢ \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])) \to (\forall x \in On A ∖ F [x] \neq \emptyset \to \forall x \in On F (x) \in (A ∖ F [x]))$
6	2 5	sylbi	$⊢ φ \to (\forall x \in On A ∖ F [x] \neq \emptyset \to \forall x \in On F (x) \in (A ∖ F [x]))$
7	4 6	biimtrrid	$⊢ φ \to (\forall x \in On \neg A ∖ F [x] = \emptyset \to \forall x \in On F (x) \in (A ∖ F [x]))$
8	1	tz7.48-3	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to \neg A \in V$
9		elex	$⊢ A \in B \to A \in V$
10	8 9	nsyl3	$⊢ A \in B \to \neg \forall x \in On F (x) \in (A ∖ F [x])$
11	7 10	nsyli	$⊢ φ \to (A \in B \to \neg \forall x \in On \neg A ∖ F [x] = \emptyset)$
12		dfrex2	$⊢ \exists x \in On A ∖ F [x] = \emptyset \leftrightarrow \neg \forall x \in On \neg A ∖ F [x] = \emptyset$
13	11 12	syl6ibr	$⊢ φ \to (A \in B \to \exists x \in On A ∖ F [x] = \emptyset)$
14		imaeq2	$⊢ x = y \to F [x] = F [y]$
15	14	difeq2d	$⊢ x = y \to A ∖ F [x] = A ∖ F [y]$
16	15	eqeq1d	$⊢ x = y \to (A ∖ F [x] = \emptyset \leftrightarrow A ∖ F [y] = \emptyset)$
17	16	onminex	$⊢ \exists x \in On A ∖ F [x] = \emptyset \to \exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x \neg A ∖ F [y] = \emptyset)$
18	13 17	syl6	$⊢ φ \to (A \in B \to \exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x \neg A ∖ F [y] = \emptyset))$
19		df-ne	$⊢ A ∖ F [y] \neq \emptyset \leftrightarrow \neg A ∖ F [y] = \emptyset$
20	19	ralbii	$⊢ \forall y \in x A ∖ F [y] \neq \emptyset \leftrightarrow \forall y \in x \neg A ∖ F [y] = \emptyset$
21	20	anbi2i	$⊢ (A ∖ F [x] = \emptyset \land \forall y \in x A ∖ F [y] \neq \emptyset) \leftrightarrow (A ∖ F [x] = \emptyset \land \forall y \in x \neg A ∖ F [y] = \emptyset)$
22	21	rexbii	$⊢ \exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x A ∖ F [y] \neq \emptyset) \leftrightarrow \exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x \neg A ∖ F [y] = \emptyset)$
23	18 22	syl6ibr	$⊢ φ \to (A \in B \to \exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x A ∖ F [y] \neq \emptyset))$
24		nfra1	$⊢ Ⅎ x \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
25	2 24	nfxfr	$⊢ Ⅎ x φ$
26		simpllr	$⊢ (((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \land A ∖ F [x] = \emptyset) \to \forall y \in x A ∖ F [y] \neq \emptyset$
27		fnfun	$⊢ F Fn On \to Fun F$
28	1 27	ax-mp	$⊢ Fun F$
29		fvelima	$⊢ (Fun F \land z \in F [x]) \to \exists y \in x F (y) = z$
30	28 29	mpan	$⊢ z \in F [x] \to \exists y \in x F (y) = z$
31		nfv	$⊢ Ⅎ y φ$
32		nfra1	$⊢ Ⅎ y \forall y \in x A ∖ F [y] \neq \emptyset$
33	31 32	nfan	$⊢ Ⅎ y (φ \land \forall y \in x A ∖ F [y] \neq \emptyset)$
34		nfv	$⊢ Ⅎ y (x \in On \to z \in A)$
35		rsp	$⊢ \forall y \in x A ∖ F [y] \neq \emptyset \to (y \in x \to A ∖ F [y] \neq \emptyset)$
36	35	adantld	$⊢ \forall y \in x A ∖ F [y] \neq \emptyset \to ((x \in On \land y \in x) \to A ∖ F [y] \neq \emptyset)$
37		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
38	15	neeq1d	$⊢ x = y \to (A ∖ F [x] \neq \emptyset \leftrightarrow A ∖ F [y] \neq \emptyset)$
39		fveq2	$⊢ x = y \to F (x) = F (y)$
40	39 15	eleq12d	$⊢ x = y \to (F (x) \in (A ∖ F [x]) \leftrightarrow F (y) \in (A ∖ F [y]))$
41	38 40	imbi12d	$⊢ x = y \to ((A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])) \leftrightarrow (A ∖ F [y] \neq \emptyset \to F (y) \in (A ∖ F [y])))$
42	41	rspcv	$⊢ y \in On \to (\forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])) \to (A ∖ F [y] \neq \emptyset \to F (y) \in (A ∖ F [y])))$
43	2 42	biimtrid	$⊢ y \in On \to (φ \to (A ∖ F [y] \neq \emptyset \to F (y) \in (A ∖ F [y])))$
44	43	com23	$⊢ y \in On \to (A ∖ F [y] \neq \emptyset \to (φ \to F (y) \in (A ∖ F [y])))$
45	37 44	syl	$⊢ (x \in On \land y \in x) \to (A ∖ F [y] \neq \emptyset \to (φ \to F (y) \in (A ∖ F [y])))$
46	36 45	sylcom	$⊢ \forall y \in x A ∖ F [y] \neq \emptyset \to ((x \in On \land y \in x) \to (φ \to F (y) \in (A ∖ F [y])))$
47	46	com3r	$⊢ φ \to (\forall y \in x A ∖ F [y] \neq \emptyset \to ((x \in On \land y \in x) \to F (y) \in (A ∖ F [y])))$
48	47	imp	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to ((x \in On \land y \in x) \to F (y) \in (A ∖ F [y]))$
49	48	expcomd	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (y \in x \to (x \in On \to F (y) \in (A ∖ F [y])))$
50		eldifi	$⊢ F (y) \in (A ∖ F [y]) \to F (y) \in A$
51		eleq1	$⊢ F (y) = z \to (F (y) \in A \leftrightarrow z \in A)$
52	50 51	syl5ibcom	$⊢ F (y) \in (A ∖ F [y]) \to (F (y) = z \to z \in A)$
53	49 52	syl8	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (y \in x \to (x \in On \to (F (y) = z \to z \in A)))$
54	53	com34	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (y \in x \to (F (y) = z \to (x \in On \to z \in A)))$
55	33 34 54	rexlimd	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (\exists y \in x F (y) = z \to (x \in On \to z \in A))$
56	30 55	syl5	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (z \in F [x] \to (x \in On \to z \in A))$
57	56	com23	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (x \in On \to (z \in F [x] \to z \in A))$
58	57	imp	$⊢ ((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \to (z \in F [x] \to z \in A)$
59	58	ssrdv	$⊢ ((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \to F [x] \subseteq A$
60		ssdif0	$⊢ A \subseteq F [x] \leftrightarrow A ∖ F [x] = \emptyset$
61	60	biimpri	$⊢ A ∖ F [x] = \emptyset \to A \subseteq F [x]$
62	59 61	anim12i	$⊢ (((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \land A ∖ F [x] = \emptyset) \to (F [x] \subseteq A \land A \subseteq F [x])$
63		eqss	$⊢ F [x] = A \leftrightarrow (F [x] \subseteq A \land A \subseteq F [x])$
64	62 63	sylibr	$⊢ (((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \land A ∖ F [x] = \emptyset) \to F [x] = A$
65		onss	$⊢ x \in On \to x \subseteq On$
66	32 31	nfan	$⊢ Ⅎ y (\forall y \in x A ∖ F [y] \neq \emptyset \land φ)$
67		nfv	$⊢ Ⅎ y x \subseteq On$
68	66 67	nfan	$⊢ Ⅎ y ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On)$
69		nfv	$⊢ Ⅎ z (((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On) \land y \in x)$
70		ssel	$⊢ x \subseteq On \to (y \in x \to y \in On)$
71		onss	$⊢ y \in On \to y \subseteq On$
72	1	fndmi	$⊢ dom F = On$
73	71 72	sseqtrrdi	$⊢ y \in On \to y \subseteq dom F$
74		funfvima2	$⊢ (Fun F \land y \subseteq dom F) \to (z \in y \to F (z) \in F [y])$
75	28 73 74	sylancr	$⊢ y \in On \to (z \in y \to F (z) \in F [y])$
76	70 75	syl6	$⊢ x \subseteq On \to (y \in x \to (z \in y \to F (z) \in F [y]))$
77	35	com12	$⊢ y \in x \to (\forall y \in x A ∖ F [y] \neq \emptyset \to A ∖ F [y] \neq \emptyset)$
78	77	a1i	$⊢ x \subseteq On \to (y \in x \to (\forall y \in x A ∖ F [y] \neq \emptyset \to A ∖ F [y] \neq \emptyset))$
79	70 78 44	syl10	$⊢ x \subseteq On \to (y \in x \to (\forall y \in x A ∖ F [y] \neq \emptyset \to (φ \to F (y) \in (A ∖ F [y]))))$
80	79	imp4a	$⊢ x \subseteq On \to (y \in x \to ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to F (y) \in (A ∖ F [y])))$
81		eldifn	$⊢ F (y) \in (A ∖ F [y]) \to \neg F (y) \in F [y]$
82		eleq1a	$⊢ F (z) \in F [y] \to (F (y) = F (z) \to F (y) \in F [y])$
83	82	con3d	$⊢ F (z) \in F [y] \to (\neg F (y) \in F [y] \to \neg F (y) = F (z))$
84	81 83	syl5com	$⊢ F (y) \in (A ∖ F [y]) \to (F (z) \in F [y] \to \neg F (y) = F (z))$
85	80 84	syl8	$⊢ x \subseteq On \to (y \in x \to ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to (F (z) \in F [y] \to \neg F (y) = F (z))))$
86	85	com34	$⊢ x \subseteq On \to (y \in x \to (F (z) \in F [y] \to ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to \neg F (y) = F (z))))$
87	76 86	syldd	$⊢ x \subseteq On \to (y \in x \to (z \in y \to ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to \neg F (y) = F (z))))$
88	87	com4r	$⊢ (\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to (x \subseteq On \to (y \in x \to (z \in y \to \neg F (y) = F (z))))$
89	88	imp31	$⊢ (((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On) \land y \in x) \to (z \in y \to \neg F (y) = F (z))$
90	69 89	ralrimi	$⊢ (((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On) \land y \in x) \to \forall z \in y \neg F (y) = F (z)$
91	90	ex	$⊢ ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On) \to (y \in x \to \forall z \in y \neg F (y) = F (z))$
92	68 91	ralrimi	$⊢ ((\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \land x \subseteq On) \to \forall y \in x \forall z \in y \neg F (y) = F (z)$
93	92	ex	$⊢ (\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to (x \subseteq On \to \forall y \in x \forall z \in y \neg F (y) = F (z))$
94	93	ancld	$⊢ (\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to (x \subseteq On \to (x \subseteq On \land \forall y \in x \forall z \in y \neg F (y) = F (z)))$
95	1	tz7.48lem	$⊢ (x \subseteq On \land \forall y \in x \forall z \in y \neg F (y) = F (z)) \to Fun {({F ↾}_{x})}^{-1}$
96	65 94 95	syl56	$⊢ (\forall y \in x A ∖ F [y] \neq \emptyset \land φ) \to (x \in On \to Fun {({F ↾}_{x})}^{-1})$
97	96	ancoms	$⊢ (φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (x \in On \to Fun {({F ↾}_{x})}^{-1})$
98	97	imp	$⊢ ((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \to Fun {({F ↾}_{x})}^{-1}$
99	98	adantr	$⊢ (((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \land A ∖ F [x] = \emptyset) \to Fun {({F ↾}_{x})}^{-1}$
100	26 64 99	3jca	$⊢ (((φ \land \forall y \in x A ∖ F [y] \neq \emptyset) \land x \in On) \land A ∖ F [x] = \emptyset) \to (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1})$
101	100	exp41	$⊢ φ \to (\forall y \in x A ∖ F [y] \neq \emptyset \to (x \in On \to (A ∖ F [x] = \emptyset \to (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}))))$
102	101	com23	$⊢ φ \to (x \in On \to (\forall y \in x A ∖ F [y] \neq \emptyset \to (A ∖ F [x] = \emptyset \to (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}))))$
103	102	com34	$⊢ φ \to (x \in On \to (A ∖ F [x] = \emptyset \to (\forall y \in x A ∖ F [y] \neq \emptyset \to (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}))))$
104	103	imp4a	$⊢ φ \to (x \in On \to ((A ∖ F [x] = \emptyset \land \forall y \in x A ∖ F [y] \neq \emptyset) \to (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1})))$
105	25 104	reximdai	$⊢ φ \to (\exists x \in On (A ∖ F [x] = \emptyset \land \forall y \in x A ∖ F [y] \neq \emptyset) \to \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}))$
106	23 105	syld	$⊢ φ \to (A \in B \to \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}))$
107	106	impcom	$⊢ (A \in B \land φ) \to \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1})$

Metamath Proof Explorer

Theorem tz7.49

Proof