fnse

Description: Condition for the well-order in fnwe to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypotheses	fnse.1	$⊢ T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))\}$
	fnse.2	$⊢ φ \to F : A ⟶ B$
	fnse.3	$⊢ φ \to R Se B$
	fnse.4	$⊢ φ \to F^{-1} [w] \in V$
Assertion	fnse	$⊢ φ \to T Se A$

Proof

Step	Hyp	Ref	Expression
1		fnse.1	$⊢ T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))\}$
2		fnse.2	$⊢ φ \to F : A ⟶ B$
3		fnse.3	$⊢ φ \to R Se B$
4		fnse.4	$⊢ φ \to F^{-1} [w] \in V$
5	2	ffvelcdmda	$⊢ (φ \land z \in A) \to F (z) \in B$
6		seex	$⊢ (R Se B \land F (z) \in B) \to \{u \in B \| u R F (z)\} \in V$
7	3 5 6	syl2an2r	$⊢ (φ \land z \in A) \to \{u \in B \| u R F (z)\} \in V$
8		snex	$⊢ \{F (z)\} \in V$
9		unexg	$⊢ (\{u \in B \| u R F (z)\} \in V \land \{F (z)\} \in V) \to \{u \in B \| u R F (z)\} \cup \{F (z)\} \in V$
10	7 8 9	sylancl	$⊢ (φ \land z \in A) \to \{u \in B \| u R F (z)\} \cup \{F (z)\} \in V$
11		imaeq2	$⊢ w = \{u \in B \| u R F (z)\} \cup \{F (z)\} \to F^{-1} [w] = F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}]$
12	11	eleq1d	$⊢ w = \{u \in B \| u R F (z)\} \cup \{F (z)\} \to (F^{-1} [w] \in V \leftrightarrow F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \in V)$
13	12	imbi2d	$⊢ w = \{u \in B \| u R F (z)\} \cup \{F (z)\} \to ((φ \to F^{-1} [w] \in V) \leftrightarrow (φ \to F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \in V))$
14	13 4	vtoclg	$⊢ \{u \in B \| u R F (z)\} \cup \{F (z)\} \in V \to (φ \to F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \in V)$
15	14	impcom	$⊢ (φ \land \{u \in B \| u R F (z)\} \cup \{F (z)\} \in V) \to F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \in V$
16	10 15	syldan	$⊢ (φ \land z \in A) \to F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \in V$
17		inss2	$⊢ A \cap T^{-1} [\{z\}] \subseteq T^{-1} [\{z\}]$
18		vex	$⊢ w \in V$
19	18	eliniseg	$⊢ z \in V \to (w \in T^{-1} [\{z\}] \leftrightarrow w T z)$
20	19	elv	$⊢ w \in T^{-1} [\{z\}] \leftrightarrow w T z$
21		fveq2	$⊢ x = w \to F (x) = F (w)$
22		fveq2	$⊢ y = z \to F (y) = F (z)$
23	21 22	breqan12d	$⊢ (x = w \land y = z) \to (F (x) R F (y) \leftrightarrow F (w) R F (z))$
24	21 22	eqeqan12d	$⊢ (x = w \land y = z) \to (F (x) = F (y) \leftrightarrow F (w) = F (z))$
25		breq12	$⊢ (x = w \land y = z) \to (x S y \leftrightarrow w S z)$
26	24 25	anbi12d	$⊢ (x = w \land y = z) \to ((F (x) = F (y) \land x S y) \leftrightarrow (F (w) = F (z) \land w S z))$
27	23 26	orbi12d	$⊢ (x = w \land y = z) \to ((F (x) R F (y) \lor (F (x) = F (y) \land x S y)) \leftrightarrow (F (w) R F (z) \lor (F (w) = F (z) \land w S z)))$
28	27 1	brab2a	$⊢ w T z \leftrightarrow ((w \in A \land z \in A) \land (F (w) R F (z) \lor (F (w) = F (z) \land w S z)))$
29	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in B$
30	29	adantrr	$⊢ (φ \land (w \in A \land z \in A)) \to F (w) \in B$
31		breq1	$⊢ u = F (w) \to (u R F (z) \leftrightarrow F (w) R F (z))$
32	31	elrab3	$⊢ F (w) \in B \to (F (w) \in \{u \in B \| u R F (z)\} \leftrightarrow F (w) R F (z))$
33	30 32	syl	$⊢ (φ \land (w \in A \land z \in A)) \to (F (w) \in \{u \in B \| u R F (z)\} \leftrightarrow F (w) R F (z))$
34	33	biimprd	$⊢ (φ \land (w \in A \land z \in A)) \to (F (w) R F (z) \to F (w) \in \{u \in B \| u R F (z)\})$
35		simpl	$⊢ (F (w) = F (z) \land w S z) \to F (w) = F (z)$
36		fvex	$⊢ F (w) \in V$
37	36	elsn	$⊢ F (w) \in \{F (z)\} \leftrightarrow F (w) = F (z)$
38	35 37	sylibr	$⊢ (F (w) = F (z) \land w S z) \to F (w) \in \{F (z)\}$
39	38	a1i	$⊢ (φ \land (w \in A \land z \in A)) \to ((F (w) = F (z) \land w S z) \to F (w) \in \{F (z)\})$
40	34 39	orim12d	$⊢ (φ \land (w \in A \land z \in A)) \to ((F (w) R F (z) \lor (F (w) = F (z) \land w S z)) \to (F (w) \in \{u \in B \| u R F (z)\} \lor F (w) \in \{F (z)\}))$
41		elun	$⊢ F (w) \in (\{u \in B \| u R F (z)\} \cup \{F (z)\}) \leftrightarrow (F (w) \in \{u \in B \| u R F (z)\} \lor F (w) \in \{F (z)\})$
42	40 41	imbitrrdi	$⊢ (φ \land (w \in A \land z \in A)) \to ((F (w) R F (z) \lor (F (w) = F (z) \land w S z)) \to F (w) \in (\{u \in B \| u R F (z)\} \cup \{F (z)\}))$
43		simprl	$⊢ (φ \land (w \in A \land z \in A)) \to w \in A$
44	42 43	jctild	$⊢ (φ \land (w \in A \land z \in A)) \to ((F (w) R F (z) \lor (F (w) = F (z) \land w S z)) \to (w \in A \land F (w) \in (\{u \in B \| u R F (z)\} \cup \{F (z)\})))$
45	2	ffnd	$⊢ φ \to F Fn A$
46	45	adantr	$⊢ (φ \land (w \in A \land z \in A)) \to F Fn A$
47		elpreima	$⊢ F Fn A \to (w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \leftrightarrow (w \in A \land F (w) \in (\{u \in B \| u R F (z)\} \cup \{F (z)\})))$
48	46 47	syl	$⊢ (φ \land (w \in A \land z \in A)) \to (w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}] \leftrightarrow (w \in A \land F (w) \in (\{u \in B \| u R F (z)\} \cup \{F (z)\})))$
49	44 48	sylibrd	$⊢ (φ \land (w \in A \land z \in A)) \to ((F (w) R F (z) \lor (F (w) = F (z) \land w S z)) \to w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}])$
50	49	expimpd	$⊢ φ \to (((w \in A \land z \in A) \land (F (w) R F (z) \lor (F (w) = F (z) \land w S z))) \to w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}])$
51	28 50	biimtrid	$⊢ φ \to (w T z \to w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}])$
52	20 51	biimtrid	$⊢ φ \to (w \in T^{-1} [\{z\}] \to w \in F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}])$
53	52	ssrdv	$⊢ φ \to T^{-1} [\{z\}] \subseteq F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}]$
54	17 53	sstrid	$⊢ φ \to A \cap T^{-1} [\{z\}] \subseteq F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}]$
55	54	adantr	$⊢ (φ \land z \in A) \to A \cap T^{-1} [\{z\}] \subseteq F^{-1} [\{u \in B \| u R F (z)\} \cup \{F (z)\}]$
56	16 55	ssexd	$⊢ (φ \land z \in A) \to A \cap T^{-1} [\{z\}] \in V$
57	56	ralrimiva	$⊢ φ \to \forall z \in A A \cap T^{-1} [\{z\}] \in V$
58		dfse2	$⊢ T Se A \leftrightarrow \forall z \in A A \cap T^{-1} [\{z\}] \in V$
59	57 58	sylibr	$⊢ φ \to T Se A$

Metamath Proof Explorer

Theorem fnse

Proof