Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tz7.49 2997

Description: Proposition 7.49 of [TakeutiZaring] p. 51.

**Hypotheses**
Ref	Expression
tz7.48.1	⊢ F Fn On
tz7.49.2	⊢ A ∈ V

**Assertion**
Ref	Expression
tz7.49	⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∃x ∈ On (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x)))

Distinct variable group(s): x,y,F x,A,y

**Proof of Theorem tz7.49**
Step	Hyp	Ref	Expression
1		tz7.49.2	. . . . . 6 ⊢ A ∈ V
2		tz7.48.1	. . . . . . 7 ⊢ F Fn On
3	2	tz7.48-3 2996	. . . . . 6 ⊢ (∀x ∈ On (F ‘x) ∈ (A ∖ (F “ x)) → ¬ A ∈ V)
4	1, 3	mt2 96	. . . . 5 ⊢ ¬ ∀x ∈ On (F ‘x) ∈ (A ∖ (F “ x))
5		r19.20 1251	. . . . 5 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (∀x ∈ On ¬ (A ∖ (F “ x)) = ∅ → ∀x ∈ On (F ‘x) ∈ (A ∖ (F “ x))))
6	4, 5	mtoi 94	. . . 4 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ¬ ∀x ∈ On ¬ (A ∖ (F “ x)) = ∅)
7		dfrex2 1212	. . . 4 ⊢ (∃x ∈ On (A ∖ (F “ x)) = ∅ ↔ ¬ ∀x ∈ On ¬ (A ∖ (F “ x)) = ∅)
8	6, 7	sylibr 175	. . 3 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∃x ∈ On (A ∖ (F “ x)) = ∅)
9		imaeq2 2603	. . . . . 6 ⊢ (x = y → (F “ x) = (F “ y))
10	9	difeq2d 1588	. . . . 5 ⊢ (x = y → (A ∖ (F “ x)) = (A ∖ (F “ y)))
11	10	cleq1d 1109	. . . 4 ⊢ (x = y → ((A ∖ (F “ x)) = ∅ ↔ (A ∖ (F “ y)) = ∅))
12	11	onminex 2275	. . 3 ⊢ (∃x ∈ On (A ∖ (F “ x)) = ∅ → ∃x ∈ On ((A ∖ (F “ x)) = ∅ ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅))
13	8, 12	syl 12	. 2 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∃x ∈ On ((A ∖ (F “ x)) = ∅ ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅))
14		hbra1 1237	. . 3 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∀x∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))))
15		pm3.27 260	. . . . . . . . 9 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅)
16	15	ad2antll 320	. . . . . . . 8 ⊢ ((((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) ∧ (A ∖ (F “ x)) = ∅) → ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅)
17		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∀y∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))))
18		hbra1 1237	. . . . . . . . . . . . . . . 16 ⊢ (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → ∀y∀y ∈ x ¬ (A ∖ (F “ y)) = ∅)
19	17, 18	hban 704	. . . . . . . . . . . . . . 15 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → ∀y(∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅))
20		ax-17 925	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On → z ∈ A) → ∀y(x ∈ On → z ∈ A))
21	11	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (x = y → (¬ (A ∖ (F “ x)) = ∅ ↔ ¬ (A ∖ (F “ y)) = ∅))
22		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x = y → (F ‘x) = (F ‘y))
23	22, 10	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (x = y → ((F ‘x) ∈ (A ∖ (F “ x)) ↔ (F ‘y) ∈ (A ∖ (F “ y))))
24	21, 23	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x = y → ((¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ↔ (¬ (A ∖ (F “ y)) = ∅ → (F ‘y) ∈ (A ∖ (F “ y)))))
25	24	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (y ∈ On → (¬ (A ∖ (F “ y)) = ∅ → (F ‘y) ∈ (A ∖ (F “ y)))))
26		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((F ‘y) = z → ((F ‘y) ∈ A ↔ z ∈ A))
27		eldifi 1591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((F ‘y) ∈ (A ∖ (F “ y)) → (F ‘y) ∈ A)
28	26, 27	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((F ‘y) = z → ((F ‘y) ∈ (A ∖ (F “ y)) → z ∈ A))
29	28	com12 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F ‘y) ∈ (A ∖ (F “ y)) → ((F ‘y) = z → z ∈ A))
30	25, 29	syl8 25	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (y ∈ On → (¬ (A ∖ (F “ y)) = ∅ → ((F ‘y) = z → z ∈ A))))
31		onelon 2223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x ∈ On ∧ y ∈ x) → y ∈ On)
32	31	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ x ∧ x ∈ On) → y ∈ On)
33	30, 32	syl5 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((y ∈ x ∧ x ∈ On) → (¬ (A ∖ (F “ y)) = ∅ → ((F ‘y) = z → z ∈ A))))
34		ra4 1243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (y ∈ x → ¬ (A ∖ (F “ y)) = ∅))
35	34	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ¬ (A ∖ (F “ y)) = ∅)
36	33, 35	syl7 24	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((y ∈ x ∧ x ∈ On) → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ((F ‘y) = z → z ∈ A))))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ((y ∈ x ∧ x ∈ On) → ((F ‘y) = z → z ∈ A))))
38	37	exp4a 295	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → (y ∈ x → (x ∈ On → ((F ‘y) = z → z ∈ A)))))
39	38	exp3a 292	. . . . . . . . . . . . . . . . . 18 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (y ∈ x → (y ∈ x → (x ∈ On → ((F ‘y) = z → z ∈ A))))))
40	39	imp 277	. . . . . . . . . . . . . . . . 17 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (y ∈ x → (y ∈ x → (x ∈ On → ((F ‘y) = z → z ∈ A)))))
41	40	pm2.43d 59	. . . . . . . . . . . . . . . 16 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (y ∈ x → (x ∈ On → ((F ‘y) = z → z ∈ A))))
42	41	com34 36	. . . . . . . . . . . . . . 15 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (y ∈ x → ((F ‘y) = z → (x ∈ On → z ∈ A))))
43	19, 20, 42	r19.23ad 1285	. . . . . . . . . . . . . 14 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (∃y ∈ x (F ‘y) = z → (x ∈ On → z ∈ A)))
44		fnfun 2721	. . . . . . . . . . . . . . . 16 ⊢ (F Fn On → Fun F)
45	2, 44	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ Fun F
46		fvelima 2859	. . . . . . . . . . . . . . 15 ⊢ ((Fun F ∧ z ∈ (F “ x)) → ∃y ∈ x (F ‘y) = z)
47	45, 46	mpan 518	. . . . . . . . . . . . . 14 ⊢ (z ∈ (F “ x) → ∃y ∈ x (F ‘y) = z)
48	43, 47	syl5 22	. . . . . . . . . . . . 13 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (z ∈ (F “ x) → (x ∈ On → z ∈ A)))
49	48	com23 32	. . . . . . . . . . . 12 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (x ∈ On → (z ∈ (F “ x) → z ∈ A)))
50	49	imp 277	. . . . . . . . . . 11 ⊢ (((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) → (z ∈ (F “ x) → z ∈ A))
51	50	ssrdv 1509	. . . . . . . . . 10 ⊢ (((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) → (F “ x) ⊆ A)
52		ssdif0 1748	. . . . . . . . . . 11 ⊢ (A ⊆ (F “ x) ↔ (A ∖ (F “ x)) = ∅)
53	52	biimpr 134	. . . . . . . . . 10 ⊢ ((A ∖ (F “ x)) = ∅ → A ⊆ (F “ x))
54	51, 53	anim12i 268	. . . . . . . . 9 ⊢ ((((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) ∧ (A ∖ (F “ x)) = ∅) → ((F “ x) ⊆ A ∧ A ⊆ (F “ x)))
55		eqss 1516	. . . . . . . . 9 ⊢ ((F “ x) = A ↔ ((F “ x) ⊆ A ∧ A ⊆ (F “ x)))
56	54, 55	sylibr 175	. . . . . . . 8 ⊢ ((((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) ∧ (A ∖ (F “ x)) = ∅) → (F “ x) = A)
57	18, 17	hban 704	. . . . . . . . . . . . . . . 16 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → ∀y(∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))))
58		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (x ⊆ On → ∀y x ⊆ On)
59		ssel 1502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ⊆ On → (y ∈ x → y ∈ On))
60		onsst 2243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y ∈ On → y ⊆ On)
61		fndm 2723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (F Fn On → dom F = On)
62	2, 61	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ dom F = On
63	60, 62	syl6ssr 1547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y ∈ On → y ⊆ dom F)
64		funfvima2 2905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Fun F ∧ y ⊆ dom F) → (z ∈ y → (F ‘z) ∈ (F “ y)))
65	45, 64	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y ⊆ dom F → (z ∈ y → (F ‘z) ∈ (F “ y)))
66	63, 65	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y ∈ On → (z ∈ y → (F ‘z) ∈ (F “ y)))
67		eldifn 1592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((F ‘y) ∈ (A ∖ (F “ y)) → ¬ (F ‘y) ∈ (F “ y))
68	25, 67	syl8 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (y ∈ On → (¬ (A ∖ (F “ y)) = ∅ → ¬ (F ‘y) ∈ (F “ y))))
69	68, 35	syl7 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (y ∈ On → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ¬ (F ‘y) ∈ (F “ y))))
70	69	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y ∈ On → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ¬ (F ‘y) ∈ (F “ y))))
71	70	imp3a 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y ∈ On → ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x)) → ¬ (F ‘y) ∈ (F “ y)))
72	66, 71	anim12d 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (y ∈ On → ((z ∈ y ∧ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x))) → ((F ‘z) ∈ (F “ y) ∧ ¬ (F ‘y) ∈ (F “ y))))
73		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((F ‘z) ∈ (F “ y) → ((F ‘y) = (F ‘z) → (F ‘y) ∈ (F “ y)))
74	73	con3d 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((F ‘z) ∈ (F “ y) → (¬ (F ‘y) ∈ (F “ y) → ¬ (F ‘y) = (F ‘z)))
75	74	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((F ‘z) ∈ (F “ y) ∧ ¬ (F ‘y) ∈ (F “ y)) → ¬ (F ‘y) = (F ‘z))
76	72, 75	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y ∈ On → ((z ∈ y ∧ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x))) → ¬ (F ‘y) = (F ‘z)))
77	76	exp4d 298	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (y ∈ On → (z ∈ y → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → ¬ (F ‘y) = (F ‘z)))))
78	77	com24 37	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ On → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (z ∈ y → ¬ (F ‘y) = (F ‘z)))))
79	59, 78	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x ⊆ On → (y ∈ x → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ y ∈ x) → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (z ∈ y → ¬ (F ‘y) = (F ‘z))))))
80	79	exp4a 295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x ⊆ On → (y ∈ x → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (y ∈ x → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (z ∈ y → ¬ (F ‘y) = (F ‘z)))))))
81	80	com34 36	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x ⊆ On → (y ∈ x → (y ∈ x → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (z ∈ y → ¬ (F ‘y) = (F ‘z)))))))
82	81	pm2.43d 59	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ⊆ On → (y ∈ x → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (z ∈ y → ¬ (F ‘y) = (F ‘z))))))
83	82	imp4a 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ⊆ On → (y ∈ x → ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (z ∈ y → ¬ (F ‘y) = (F ‘z)))))
84	83	com3r 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → (y ∈ x → (z ∈ y → ¬ (F ‘y) = (F ‘z)))))
85	84	imp4a 282	. . . . . . . . . . . . . . . . 17 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → ((y ∈ x ∧ z ∈ y) → ¬ (F ‘y) = (F ‘z))))
86	85	19.21adv 945	. . . . . . . . . . . . . . . 16 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → ∀z((y ∈ x ∧ z ∈ y) → ¬ (F ‘y) = (F ‘z))))
87	57, 58, 86	19.21ad 741	. . . . . . . . . . . . . . 15 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → ∀y∀z((y ∈ x ∧ z ∈ y) → ¬ (F ‘y) = (F ‘z))))
88		r2al 1231	. . . . . . . . . . . . . . 15 ⊢ (∀y ∈ x ∀z ∈ y ¬ (F ‘y) = (F ‘z) ↔ ∀y∀z((y ∈ x ∧ z ∈ y) → ¬ (F ‘y) = (F ‘z)))
89	87, 88	syl6ibr 186	. . . . . . . . . . . . . 14 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → ∀y ∈ x ∀z ∈ y ¬ (F ‘y) = (F ‘z)))
90	89	ancld 246	. . . . . . . . . . . . 13 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → (x ⊆ On ∧ ∀y ∈ x ∀z ∈ y ¬ (F ‘y) = (F ‘z))))
91	2	tz7.48lem 2993	. . . . . . . . . . . . 13 ⊢ ((x ⊆ On ∧ ∀y ∈ x ∀z ∈ y ¬ (F ‘y) = (F ‘z)) → Fun ^◡(F ↾ x))
92	90, 91	syl6 23	. . . . . . . . . . . 12 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ⊆ On → Fun ^◡(F ↾ x)))
93		onsst 2243	. . . . . . . . . . . 12 ⊢ (x ∈ On → x ⊆ On)
94	92, 93	syl5 22	. . . . . . . . . . 11 ⊢ ((∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ ∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x)))) → (x ∈ On → Fun ^◡(F ↾ x)))
95	94	ancoms 334	. . . . . . . . . 10 ⊢ ((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (x ∈ On → Fun ^◡(F ↾ x)))
96	95	imp 277	. . . . . . . . 9 ⊢ (((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) → Fun ^◡(F ↾ x))
97	96	adantr 306	. . . . . . . 8 ⊢ ((((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) ∧ (A ∖ (F “ x)) = ∅) → Fun ^◡(F ↾ x))
98	16, 56, 97	3jca 604	. . . . . . 7 ⊢ ((((∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) ∧ x ∈ On) ∧ (A ∖ (F “ x)) = ∅) → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x)))
99	98	exp41 299	. . . . . 6 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (x ∈ On → ((A ∖ (F “ x)) = ∅ → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x))))))
100	99	com23 32	. . . . 5 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (x ∈ On → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → ((A ∖ (F “ x)) = ∅ → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x))))))
101	100	com34 36	. . . 4 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (x ∈ On → ((A ∖ (F “ x)) = ∅ → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x))))))
102	101	imp4a 282	. . 3 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (x ∈ On → (((A ∖ (F “ x)) = ∅ ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x)))))
103	14, 102	r19.22d 1276	. 2 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → (∃x ∈ On ((A ∖ (F “ x)) = ∅ ∧ ∀y ∈ x ¬ (A ∖ (F “ y)) = ∅) → ∃x ∈ On (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x))))
104	13, 103	mpd 46	1 ⊢ (∀x ∈ On (¬ (A ∖ (F “ x)) = ∅ → (F ‘x) ∈ (A ∖ (F “ x))) → ∃x ∈ On (∀y ∈ x ¬ (A ∖ (F “ y)) = ∅ ∧ (F “ x) = A ∧ Fun ^◡(F ↾ x)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ∧ wa 196 ∧ w3a 581 ∀wal 672 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 Vcvv 1348 ∖ cdif 1484 ⊆ wss 1487 ∅c0 1707 Oncon0 2199 ^◡ccnv 2409 dom cdm 2410 ↾ cres 2412 “ cima 2413 Fun wfun 2416 Fn wfn 2417 ‘cfv 2422

This theorem is referenced by: tz7.49c 2998

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438

metamath.org